harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/SpecialFunctions/Gaussian/FourierTransform.lean
theorem integral_cexp_neg_mul_sq_norm_add
    (hb : 0 < b.re) (c : ℂ) (w : V) :
    ∫ v : V, cexp (- b * ‖v‖^2 + c * ⟪w, v⟫) =
      (π / b) ^ (Module.finrank ℝ V / 2 : ℂ) * cexp (c ^ 2 * ‖w‖^2 / (4 * b))

Proof state:
b : ℂ
V : Type u_1
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : FiniteDimensional ℝ V
inst✝¹ : MeasurableSpace V
inst✝ : BorelSpace V
hb : 0 < b.re
c : ℂ
w : V
e : EuclideanSpace ℝ (Fin (Module.finrank ℝ V)) ≃ₗᵢ[ℝ] V := (stdOrthonormalBasis ℝ V).repr.symm
⊢ ∫ (v : V), cexp (-b * ↑‖v‖ ^ 2 + c * ↑(inner w v)) =
    (↑π / b) ^ (↑(Module.finrank ℝ V) / 2) * cexp (c ^ 2 * ↑‖w‖ ^ 2 / (4 * b))

Tactic:
rw [← e.measurePreserving.integral_comp e.toHomeomorph.measurableEmbedding]

Result:
b : ℂ
V : Type u_1
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : FiniteDimensional ℝ V
inst✝¹ : MeasurableSpace V
inst✝ : BorelSpace V
hb : 0 < b.re
c : ℂ
w : V
e : EuclideanSpace ℝ (Fin (Module.finrank ℝ V)) ≃ₗᵢ[ℝ] V := (stdOrthonormalBasis ℝ V).repr.symm
⊢ ∫ (x : EuclideanSpace ℝ (Fin (Module.finrank ℝ V))), cexp (-b * ↑‖e x‖ ^ 2 + c * ↑(inner w (e x))) ∂volume =
    (↑π / b) ^ (↑(Module.finrank ℝ V) / 2) * cexp (c ^ 2 * ↑‖w‖ ^ 2 / (4 * b))

Proof state:
b : ℂ
V : Type u_1
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : FiniteDimensional ℝ V
inst✝¹ : MeasurableSpace V
inst✝ : BorelSpace V
hb : 0 < b.re
c : ℂ
w : V
⊢ ∫ (v : V), cexp (-b * ↑‖v‖ ^ 2 + c * ↑(inner w v)) =
    (↑π / b) ^ (↑(Module.finrank ℝ V) / 2) * cexp (c ^ 2 * ↑‖w‖ ^ 2 / (4 * b))

Tactic:
let e := (stdOrthonormalBasis ℝ V).repr.symm

Result:
b : ℂ
V : Type u_1
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : FiniteDimensional ℝ V
inst✝¹ : MeasurableSpace V
inst✝ : BorelSpace V
hb : 0 < b.re
c : ℂ
w : V
e : EuclideanSpace ℝ (Fin (Module.finrank ℝ V)) ≃ₗᵢ[ℝ] V := (stdOrthonormalBasis ℝ V).repr.symm
⊢ ∫ (v : V), cexp (-b * ↑‖v‖ ^ 2 + c * ↑(inner w v)) =
    (↑π / b) ^ (↑(Module.finrank ℝ V) / 2) * cexp (c ^ 2 * ↑‖w‖ ^ 2 / (4 * b))

Proof state:
b : ℂ
V : Type u_1
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : FiniteDimensional ℝ V
inst✝¹ : MeasurableSpace V
inst✝ : BorelSpace V
hb : 0 < b.re
c : ℂ
w : V
e : EuclideanSpace ℝ (Fin (Module.finrank ℝ V)) ≃ₗᵢ[ℝ] V := (stdOrthonormalBasis ℝ V).repr.symm
⊢ ∫ (x : EuclideanSpace ℝ (Fin (Module.finrank ℝ V))), cexp (-b * ↑‖e x‖ ^ 2 + c * ↑(inner w (e x))) ∂volume =
    (↑π / b) ^ (↑(Module.finrank ℝ V) / 2) * cexp (c ^ 2 * ↑‖w‖ ^ 2 / (4 * b))

Tactic:
convert integral_cexp_neg_mul_sq_norm_add_of_euclideanSpace
  hb c (e.symm w) <;> simp [LinearIsometryEquiv.inner_map_eq_flip]

Result:
no goals
-- Mathlib/Data/Matrix/ConjTranspose.lean
theorem conjTranspose_natCast_smul [Semiring R] [AddCommMonoid α] [StarAddMonoid α] [Module R α]
    (c : ℕ) (M : Matrix m n α) : ((c : R) • M)ᴴ = (c : R) • Mᴴ :=
  Matrix.ext <| by simp

Proof state:
m : Type u_2
n : Type u_3
R : Type u_7
α : Type v
inst✝³ : Semiring R
inst✝² : AddCommMonoid α
inst✝¹ : StarAddMonoid α
inst✝ : Module R α
c : ℕ
M : Matrix m n α
⊢ ∀ (i : n) (j : m), (↑c • M)ᴴ i j = (↑c • Mᴴ) i j

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Angle.lean
theorem two_nsmul_neg_pi_div_two : (2 : ℕ) • (↑(-π / 2) : Angle) = π

Proof state:
⊢ 2 • ↑(-π / 2) = ↑π

Tactic:
rw [two_nsmul_coe_div_two, coe_neg, neg_coe_pi]

Result:
no goals
-- Mathlib/Algebra/Group/Basic.lean
@[to_additive (attr := simp)]
lemma div_mul_cancel_right (a b : G) : a / (b * a) = b⁻¹

Proof state:
G : Type u_3
inst✝ : Group G
a b : G
⊢ a / (b * a) = b⁻¹

Tactic:
rw [← inv_div, mul_div_cancel_right]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Range.lean
theorem zipIdx_eq_nil_iff {l : List α} {n : Nat} : List.zipIdx l n = [] ↔ l = []

Proof state:
α : Type u_1
l : List α
n : Nat
⊢ l.zipIdx n = [] ↔ l = []

Tactic:
cases l <;> simp

Result:
no goals
-- Mathlib/RingTheory/Radical.lean
theorem divRadical_mul_radical (a : E) : divRadical a * radical a = a

Proof state:
E : Type u_1
inst✝² : EuclideanDomain E
inst✝¹ : NormalizationMonoid E
inst✝ : UniqueFactorizationMonoid E
a : E
⊢ divRadical a * radical a = a

Tactic:
rw [mul_comm]

Result:
E : Type u_1
inst✝² : EuclideanDomain E
inst✝¹ : NormalizationMonoid E
inst✝ : UniqueFactorizationMonoid E
a : E
⊢ radical a * divRadical a = a

Proof state:
E : Type u_1
inst✝² : EuclideanDomain E
inst✝¹ : NormalizationMonoid E
inst✝ : UniqueFactorizationMonoid E
a : E
⊢ radical a * divRadical a = a

Tactic:
exact radical_mul_divRadical a

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/Orientation.lean
theorem orientation_adjustToOrientation : (e.adjustToOrientation x).toBasis.orientation = x

Proof state:
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
ι : Type u_2
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
e : OrthonormalBasis ι ℝ E
x : Orientation ℝ E ι
inst✝ : Nonempty ι
⊢ (e.toBasis.adjustToOrientation x).orientation = x

Tactic:
exact e.toBasis.orientation_adjustToOrientation x

Result:
no goals

Proof state:
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
ι : Type u_2
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
e : OrthonormalBasis ι ℝ E
x : Orientation ℝ E ι
inst✝ : Nonempty ι
⊢ (e.adjustToOrientation x).toBasis.orientation = x

Tactic:
rw [e.toBasis_adjustToOrientation]

Result:
E : Type u_1
inst✝⁴ : NormedAddCommGroup E
inst✝³ : InnerProductSpace ℝ E
ι : Type u_2
inst✝² : Fintype ι
inst✝¹ : DecidableEq ι
e : OrthonormalBasis ι ℝ E
x : Orientation ℝ E ι
inst✝ : Nonempty ι
⊢ (e.toBasis.adjustToOrientation x).orientation = x
-- Mathlib/Algebra/BigOperators/Group/Multiset/Basic.lean
theorem prod_erase [DecidableEq α] (h : a ∈ s) : a * (s.erase a).prod = s.prod

Proof state:
α : Type u_3
inst✝¹ : CommMonoid α
s : Multiset α
a : α
inst✝ : DecidableEq α
h : a ∈ s
⊢ a * (s.erase a).prod = s.prod

Tactic:
rw [← s.coe_toList, coe_erase, prod_coe, prod_coe, List.prod_erase (mem_toList.2 h)]

Result:
no goals
-- Mathlib/Analysis/Normed/Affine/AddTorsor.lean
theorem dist_homothety_self (p₁ p₂ : P) (c : 𝕜) :
    dist (homothety p₁ c p₂) p₂ = ‖1 - c‖ * dist p₁ p₂

Proof state:
V : Type u_1
P : Type u_2
inst✝⁴ : SeminormedAddCommGroup V
inst✝³ : PseudoMetricSpace P
inst✝² : NormedAddTorsor V P
𝕜 : Type u_5
inst✝¹ : NormedField 𝕜
inst✝ : NormedSpace 𝕜 V
p₁ p₂ : P
c : 𝕜
⊢ dist ((homothety p₁ c) p₂) p₂ = ‖1 - c‖ * dist p₁ p₂

Tactic:
rw [homothety_eq_lineMap, dist_lineMap_right]

Result:
no goals
-- Mathlib/Algebra/SkewMonoidAlgebra/Basic.lean
theorem support_ofFinsupp (p) : support (⟨p⟩ : SkewMonoidAlgebra k G) = p.support

Proof state:
k : Type u_1
G : Type u_2
inst✝ : AddCommMonoid k
p : G →₀ k
⊢ { toFinsupp := p }.support = p.support

Tactic:
rw [support]

Result:
no goals
-- Mathlib/Data/ENNReal/Inv.lean
lemma mul_sSup {a : ℝ≥0∞} : a * sSup s = ⨆ b ∈ s, a * b

Proof state:
s : Set ℝ≥0∞
a : ℝ≥0∞
⊢ a * sSup s = ⨆ b ∈ s, a * b

Tactic:
simp only [sSup_eq_iSup, mul_iSup]

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Arithmetic.lean
theorem mul_add_mod_self (x y z : Ordinal) : (x * y + z) % x = z % x

Proof state:
case inr
x y z : Ordinal.{u_4}
hx : x ≠ 0
⊢ (x * y + z) % x = z % x

Tactic:
rwa [mod_def, mul_add_div, mul_add, ← sub_sub, add_sub_cancel, mod_def]

Result:
no goals

Proof state:
x y z : Ordinal.{u_4}
⊢ (x * y + z) % x = z % x

Tactic:
rcases eq_or_ne x 0 with rfl | hx

Result:
case inl
y z : Ordinal.{u_4}
⊢ (0 * y + z) % 0 = z % 0

case inr
x y z : Ordinal.{u_4}
hx : x ≠ 0
⊢ (x * y + z) % x = z % x

Proof state:
case inl
y z : Ordinal.{u_4}
⊢ (0 * y + z) % 0 = z % 0

Tactic:
simp

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Constructions/FiniteProductsOfBinaryProducts.lean
/-- If `F` preserves the terminal object and binary products, then it preserves limits of shape
`Discrete (Fin n)`.
-/
lemma preservesShape_fin_of_preserves_binary_and_terminal (n : ℕ) :
    PreservesLimitsOfShape (Discrete (Fin n)) F where
  preservesLimit {K}

Proof state:
C : Type u
inst✝⁴ : Category.{v, u} C
D : Type u'
inst✝³ : Category.{v', u'} D
F : C ⥤ D
inst✝² : PreservesLimitsOfShape (Discrete WalkingPair) F
inst✝¹ : PreservesLimitsOfShape (Discrete PEmpty.{1}) F
inst✝ : HasFiniteProducts C
n : ℕ
K : Discrete (Fin n) ⥤ C
that : (Discrete.functor fun n_1 => K.obj { as := n_1 }) ≅ K :=
  Discrete.natIso fun x =>
    match x with
    | { as := i } => Iso.refl ((Discrete.functor fun n_1 => K.obj { as := n_1 }).obj { as := i })
this : PreservesLimit (Discrete.functor fun n_1 => K.obj { as := n_1 }) F
⊢ PreservesLimit K F

Tactic:
apply preservesLimit_of_iso_diagram F that

Result:
no goals

Proof state:
C : Type u
inst✝⁴ : Category.{v, u} C
D : Type u'
inst✝³ : Category.{v', u'} D
F : C ⥤ D
inst✝² : PreservesLimitsOfShape (Discrete WalkingPair) F
inst✝¹ : PreservesLimitsOfShape (Discrete PEmpty.{1}) F
inst✝ : HasFiniteProducts C
n : ℕ
K : Discrete (Fin n) ⥤ C
that : (Discrete.functor fun n_1 => K.obj { as := n_1 }) ≅ K :=
  Discrete.natIso fun x =>
    match x with
    | { as := i } => Iso.refl ((Discrete.functor fun n_1 => K.obj { as := n_1 }).obj { as := i })
⊢ PreservesLimit K F

Tactic:
haveI := preservesFinOfPreservesBinaryAndTerminal F n fun n => K.obj ⟨n⟩

Result:
C : Type u
inst✝⁴ : Category.{v, u} C
D : Type u'
inst✝³ : Category.{v', u'} D
F : C ⥤ D
inst✝² : PreservesLimitsOfShape (Discrete WalkingPair) F
inst✝¹ : PreservesLimitsOfShape (Discrete PEmpty.{1}) F
inst✝ : HasFiniteProducts C
n : ℕ
K : Discrete (Fin n) ⥤ C
that : (Discrete.functor fun n_1 => K.obj { as := n_1 }) ≅ K :=
  Discrete.natIso fun x =>
    match x with
    | { as := i } => Iso.refl ((Discrete.functor fun n_1 => K.obj { as := n_1 }).obj { as := i })
this : PreservesLimit (Discrete.functor fun n_1 => K.obj { as := n_1 }) F
⊢ PreservesLimit K F

Proof state:
C : Type u
inst✝⁴ : Category.{v, u} C
D : Type u'
inst✝³ : Category.{v', u'} D
F : C ⥤ D
inst✝² : PreservesLimitsOfShape (Discrete WalkingPair) F
inst✝¹ : PreservesLimitsOfShape (Discrete PEmpty.{1}) F
inst✝ : HasFiniteProducts C
n : ℕ
K : Discrete (Fin n) ⥤ C
⊢ PreservesLimit K F

Tactic:
let that : (Discrete.functor fun n => K.obj ⟨n⟩) ≅ K := Discrete.natIso fun ⟨i⟩ => Iso.refl _

Result:
C : Type u
inst✝⁴ : Category.{v, u} C
D : Type u'
inst✝³ : Category.{v', u'} D
F : C ⥤ D
inst✝² : PreservesLimitsOfShape (Discrete WalkingPair) F
inst✝¹ : PreservesLimitsOfShape (Discrete PEmpty.{1}) F
inst✝ : HasFiniteProducts C
n : ℕ
K : Discrete (Fin n) ⥤ C
that : (Discrete.functor fun n_1 => K.obj { as := n_1 }) ≅ K :=
  Discrete.natIso fun x =>
    match x with
    | { as := i } => Iso.refl ((Discrete.functor fun n_1 => K.obj { as := n_1 }).obj { as := i })
⊢ PreservesLimit K F
-- Mathlib/Topology/ContinuousMap/Basic.lean
theorem liftCover_coe {i : ι} (x : S i) : liftCover S φ hφ hS x = φ i x

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
ι : Type u_5
S : ι → Set α
φ : (i : ι) → C(↑(S i), β)
hφ : ∀ (i j : ι) (x : α) (hxi : x ∈ S i) (hxj : x ∈ S j), (φ i) ⟨x, hxi⟩ = (φ j) ⟨x, hxj⟩
hS : ∀ (x : α), ∃ i, S i ∈ 𝓝 x
i : ι
x : ↑(S i)
⊢ (liftCover S φ hφ hS) ↑x = (φ i) x

Tactic:
rw [liftCover, coe_mk, Set.liftCover_coe _]

Result:
no goals
-- Mathlib/RingTheory/Radical.lean
theorem radical_mul_divRadical (a : E) : radical a * divRadical a = a

Proof state:
E : Type u_1
inst✝² : EuclideanDomain E
inst✝¹ : NormalizationMonoid E
inst✝ : UniqueFactorizationMonoid E
a : E
⊢ radical a * divRadical a = a

Tactic:
rw [divRadical, ← EuclideanDomain.mul_div_assoc _ (radical_dvd_self a),
  mul_div_cancel_left₀ _ (radical_ne_zero a)]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Preserves/Finite.lean
/-- If we preserve colimits of some arbitrary size, then we preserve all finite colimits. -/
lemma PreservesColimitsOfSize.preservesFiniteColimits (F : C ⥤ D)
    [PreservesColimitsOfSize.{w, w₂} F] : PreservesFiniteColimits F where
  preservesFiniteColimits J (sJ : SmallCategory J) fJ

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : PreservesColimitsOfSize.{w, w₂, v₁, v₂, u₁, u₂} F
J : Type
sJ : SmallCategory J
fJ : FinCategory J
this : PreservesColimitsOfSize.{0, 0, v₁, v₂, u₁, u₂} F
⊢ PreservesColimitsOfShape J F

Tactic:
exact preservesColimitsOfShape_of_equiv (FinCategory.equivAsType J) F

Result:
no goals

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : PreservesColimitsOfSize.{w, w₂, v₁, v₂, u₁, u₂} F
J : Type
sJ : SmallCategory J
fJ : FinCategory J
⊢ PreservesColimitsOfShape J F

Tactic:
haveI := preservesSmallestColimits_of_preservesColimits F

Result:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : C ⥤ D
inst✝ : PreservesColimitsOfSize.{w, w₂, v₁, v₂, u₁, u₂} F
J : Type
sJ : SmallCategory J
fJ : FinCategory J
this : PreservesColimitsOfSize.{0, 0, v₁, v₂, u₁, u₂} F
⊢ PreservesColimitsOfShape J F
-- Mathlib/CategoryTheory/Limits/Shapes/Images.lean
theorem image.preComp_ι [HasImage g] [HasImage (f ≫ g)] :
    image.preComp f g ≫ image.ι g = image.ι (f ≫ g)

Proof state:
C : Type u
inst✝² : Category.{v, u} C
X Y : C
f : X ⟶ Y
Z : C
g : Y ⟶ Z
inst✝¹ : HasImage g
inst✝ : HasImage (f ≫ g)
⊢ preComp f g ≫ ι g = ι (f ≫ g)

Tactic:
dsimp [image.preComp]

Result:
C : Type u
inst✝² : Category.{v, u} C
X Y : C
f : X ⟶ Y
Z : C
g : Y ⟶ Z
inst✝¹ : HasImage g
inst✝ : HasImage (f ≫ g)
⊢ lift (MonoFactorisation.mk (image g) (ι g) (f ≫ factorThruImage g) ⋯) ≫ ι g = ι (f ≫ g)

Proof state:
C : Type u
inst✝² : Category.{v, u} C
X Y : C
f : X ⟶ Y
Z : C
g : Y ⟶ Z
inst✝¹ : HasImage g
inst✝ : HasImage (f ≫ g)
⊢ lift (MonoFactorisation.mk (image g) (ι g) (f ≫ factorThruImage g) ⋯) ≫ ι g = ι (f ≫ g)

Tactic:
rw [image.lift_fac]

Result:
no goals
-- Mathlib/Topology/Separation/Basic.lean
theorem nhds_inter_eq_singleton_of_mem_discrete {s : Set X} [DiscreteTopology s] {x : X}
    (hx : x ∈ s) : ∃ U ∈ 𝓝 x, U ∩ s = {x}

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
s : Set X
inst✝ : DiscreteTopology ↑s
x : X
hx : x ∈ s
⊢ ∃ U ∈ 𝓝 x, U ∩ s = {x}

Tactic:
simpa using (𝓝 x).basis_sets.exists_inter_eq_singleton_of_mem_discrete hx

Result:
no goals
-- Mathlib/FieldTheory/IntermediateField/Adjoin/Basic.lean
theorem adjoinRootEquivAdjoin_symm_apply_gen (h : IsIntegral F α) :
    (adjoinRootEquivAdjoin F h).symm (AdjoinSimple.gen F α) = AdjoinRoot.root (minpoly F α)

Proof state:
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
α : E
h : IsIntegral F α
⊢ (adjoinRootEquivAdjoin F h).symm (AdjoinSimple.gen F α) = AdjoinRoot.root (minpoly F α)

Tactic:
rw [AlgEquiv.symm_apply_eq, adjoinRootEquivAdjoin_apply_root]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem any_insert [BEq α] [LawfulBEq α] {l : List α} {a : α} :
    (l.insert a).any f = (f a || l.any f)

Proof state:
α : Type u_1
f : α → Bool
inst✝¹ : BEq α
inst✝ : LawfulBEq α
l : List α
a : α
⊢ (List.insert a l).any f = (f a || l.any f)

Tactic:
simp [any_eq]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem lt_irrefl (x : BitVec n) : ¬x < x

Proof state:
n : Nat
x : BitVec n
⊢ ¬x < x

Tactic:
simp [lt_def]

Result:
no goals
-- Mathlib/Data/Sym/Sym2.lean
theorem Rel.trans {x y z : α × α} (a : Rel α x y) (b : Rel α y z) : Rel α x z

Proof state:
α : Type u_1
x y z : α × α
a : Rel α x y
b : Rel α y z
⊢ Rel α x z

Tactic:
aesop (rule_sets := [Sym2])

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem contains_insertIfNew_self [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {k : α} {v : β k} :
    (m.insertIfNew k v).contains k

Proof state:
α : Type u
β : α → Type v
m : Raw₀ α β
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.val.WF
k : α
v : β k
⊢ (m.insertIfNew k v).contains k = true

Tactic:
simp_to_model [insertIfNew] using List.containsKey_insertEntryIfNew_self

Result:
no goals
-- Mathlib/Data/Set/UnionLift.lean
theorem iUnionLift_of_mem (x : T) {i : ι} (hx : (x : α) ∈ S i) :
    iUnionLift S f hf T hT x = f i ⟨x, hx⟩

Proof state:
case mk
α : Type u_1
ι : Sort u_3
β : Sort u_2
S : ι → Set α
f : (i : ι) → ↑(S i) → β
hf : ∀ (i j : ι) (x : α) (hxi : x ∈ S i) (hxj : x ∈ S j), f i ⟨x, hxi⟩ = f j ⟨x, hxj⟩
T : Set α
hT : T ⊆ iUnion S
i : ι
x : α
hx✝ : x ∈ T
hx : ↑⟨x, hx✝⟩ ∈ S i
⊢ iUnionLift S f hf T hT ⟨x, hx✝⟩ = f i ⟨↑⟨x, hx✝⟩, hx⟩

Tactic:
exact hf _ _ _ _ _

Result:
no goals

Proof state:
α : Type u_1
ι : Sort u_3
β : Sort u_2
S : ι → Set α
f : (i : ι) → ↑(S i) → β
hf : ∀ (i j : ι) (x : α) (hxi : x ∈ S i) (hxj : x ∈ S j), f i ⟨x, hxi⟩ = f j ⟨x, hxj⟩
T : Set α
hT : T ⊆ iUnion S
x : ↑T
i : ι
hx : ↑x ∈ S i
⊢ iUnionLift S f hf T hT x = f i ⟨↑x, hx⟩

Tactic:
obtain ⟨x, hx⟩ := x

Result:
case mk
α : Type u_1
ι : Sort u_3
β : Sort u_2
S : ι → Set α
f : (i : ι) → ↑(S i) → β
hf : ∀ (i j : ι) (x : α) (hxi : x ∈ S i) (hxj : x ∈ S j), f i ⟨x, hxi⟩ = f j ⟨x, hxj⟩
T : Set α
hT : T ⊆ iUnion S
i : ι
x : α
hx✝ : x ∈ T
hx : ↑⟨x, hx✝⟩ ∈ S i
⊢ iUnionLift S f hf T hT ⟨x, hx✝⟩ = f i ⟨↑⟨x, hx✝⟩, hx⟩
-- Mathlib/CategoryTheory/Sums/Basic.lean
theorem hom_inr_inl_false {X : C} {Y : D} (f : Sum.inr X ⟶ Sum.inl Y) : False

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₁
inst✝ : Category.{v₁, u₁} D
X : C
Y : D
f : inr X ⟶ inl Y
⊢ False

Tactic:
cases f

Result:
no goals
-- Mathlib/Order/Filter/Cofinite.lean
theorem Tendsto.countable_compl_preimage_ker {f : α → β}
    {l : Filter β} [l.IsCountablyGenerated] (h : Tendsto f cofinite l) :
    Set.Countable (f ⁻¹' l.ker)ᶜ

Proof state:
α : Type u_2
β : Type u_3
f : α → β
l : Filter β
inst✝ : l.IsCountablyGenerated
h : Tendsto f cofinite l
⊢ (comap f l).kerᶜ.Countable

Tactic:
exact countable_compl_ker h.le_comap

Result:
no goals

Proof state:
α : Type u_2
β : Type u_3
f : α → β
l : Filter β
inst✝ : l.IsCountablyGenerated
h : Tendsto f cofinite l
⊢ (f ⁻¹' l.ker)ᶜ.Countable

Tactic:
rw [← ker_comap]

Result:
α : Type u_2
β : Type u_3
f : α → β
l : Filter β
inst✝ : l.IsCountablyGenerated
h : Tendsto f cofinite l
⊢ (comap f l).kerᶜ.Countable
-- Mathlib/Combinatorics/SimpleGraph/Connectivity/Subgraph.lean
theorem mem_edges_toSubgraph (p : G.Walk u v) {e : Sym2 V} :
    e ∈ p.toSubgraph.edgeSet ↔ e ∈ p.edges

Proof state:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
e : Sym2 V
⊢ e ∈ p.toSubgraph.edgeSet ↔ e ∈ p.edges

Tactic:
induction p <;> simp [*]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Omega/LinearCombo.lean
theorem add_eval (l₁ l₂ : LinearCombo) (v : Coeffs) :
    (l₁ + l₂).eval v = l₁.eval v + l₂.eval v

Proof state:
case mk
l₂ : LinearCombo
v : Coeffs
r₁ : Int
c₁ : Coeffs
⊢ ({ const := r₁, coeffs := c₁ } + l₂).eval v = { const := r₁, coeffs := c₁ }.eval v + l₂.eval v

Tactic:
rcases l₂ with ⟨r₂, c₂⟩

Result:
case mk.mk
v : Coeffs
r₁ : Int
c₁ : Coeffs
r₂ : Int
c₂ : Coeffs
⊢ ({ const := r₁, coeffs := c₁ } + { const := r₂, coeffs := c₂ }).eval v =
    { const := r₁, coeffs := c₁ }.eval v + { const := r₂, coeffs := c₂ }.eval v

Proof state:
l₁ l₂ : LinearCombo
v : Coeffs
⊢ (l₁ + l₂).eval v = l₁.eval v + l₂.eval v

Tactic:
rcases l₁ with ⟨r₁, c₁⟩

Result:
case mk
l₂ : LinearCombo
v : Coeffs
r₁ : Int
c₁ : Coeffs
⊢ ({ const := r₁, coeffs := c₁ } + l₂).eval v = { const := r₁, coeffs := c₁ }.eval v + l₂.eval v

Proof state:
case mk.mk.e_a.e_a
v : Coeffs
r₁ : Int
c₁ : Coeffs
r₂ : Int
c₂ : Coeffs
⊢ (c₁ + c₂).dot v = c₁.dot v + c₂.dot v

Tactic:
exact Coeffs.dot_distrib_left c₁ c₂ v

Result:
no goals

Proof state:
case mk.mk
v : Coeffs
r₁ : Int
c₁ : Coeffs
r₂ : Int
c₂ : Coeffs
⊢ r₁ + (r₂ + (c₁ + c₂).dot v) = r₁ + (r₂ + (c₁.dot v + c₂.dot v))

Tactic:
congr

Result:
case mk.mk.e_a.e_a
v : Coeffs
r₁ : Int
c₁ : Coeffs
r₂ : Int
c₂ : Coeffs
⊢ (c₁ + c₂).dot v = c₁.dot v + c₂.dot v

Proof state:
case mk.mk
v : Coeffs
r₁ : Int
c₁ : Coeffs
r₂ : Int
c₂ : Coeffs
⊢ ({ const := r₁, coeffs := c₁ } + { const := r₂, coeffs := c₂ }).eval v =
    { const := r₁, coeffs := c₁ }.eval v + { const := r₂, coeffs := c₂ }.eval v

Tactic:
simp only [eval, add_const, add_coeffs, Int.add_assoc, Int.add_left_comm]

Result:
case mk.mk
v : Coeffs
r₁ : Int
c₁ : Coeffs
r₂ : Int
c₂ : Coeffs
⊢ r₁ + (r₂ + (c₁ + c₂).dot v) = r₁ + (r₂ + (c₁.dot v + c₂.dot v))
-- Mathlib/Logic/Relation.lean
lemma reflTransGen_minimal {r' : α → α → Prop} (hr₁ : Reflexive r') (hr₂ : Transitive r')
    (h : ∀ x y, r x y → r' x y) {x y : α} (hxy : ReflTransGen r x y) : r' x y

Proof state:
α : Type u_1
r r' : α → α → Prop
hr₁ : Reflexive r'
hr₂ : Transitive r'
h : ∀ (x y : α), r x y → r' x y
x y : α
hxy : ReflTransGen r x y
⊢ r' x y

Tactic:
simpa [reflTransGen_eq_self hr₁ hr₂] using ReflTransGen.mono h hxy

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Connectivity/Subgraph.lean
lemma end_mem_verts_toSubgraph (p : G.Walk u v) : v ∈ p.toSubgraph.verts

Proof state:
V : Type u
G : SimpleGraph V
u v : V
p : G.Walk u v
⊢ v ∈ p.toSubgraph.verts

Tactic:
simp [mem_verts_toSubgraph]

Result:
no goals
-- Mathlib/Analysis/Quaternion.lean
theorem norm_star (a : ℍ) : ‖star a‖ = ‖a‖

Proof state:
a : ℍ
⊢ ‖star a‖ = ‖a‖

Tactic:
simp_rw [norm_eq_sqrt_real_inner, inner_self, normSq_star]

Result:
no goals
-- Mathlib/RingTheory/Polynomial/IntegralNormalization.lean
theorem integralNormalization_zero : integralNormalization (0 : R[X]) = 0

Proof state:
R : Type u
inst✝ : Semiring R
⊢ integralNormalization 0 = 0

Tactic:
simp [integralNormalization]

Result:
no goals
-- Mathlib/Topology/Compactness/LocallyCompact.lean
theorem IsOpenQuotientMap.weaklyLocallyCompactSpace [WeaklyLocallyCompactSpace X]
    {f : X → Y} (hf : IsOpenQuotientMap f) : WeaklyLocallyCompactSpace Y where
  exists_compact_mem_nhds

Proof state:
case intro.intro
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : WeaklyLocallyCompactSpace X
f : X → Y
hf : IsOpenQuotientMap f
x : X
K : Set X
hKc : IsCompact K
hKx : K ∈ 𝓝 x
⊢ ∃ s, IsCompact s ∧ s ∈ 𝓝 (f x)

Tactic:
exact ⟨f '' K, hKc.image hf.continuous, hf.isOpenMap.image_mem_nhds hKx⟩

Result:
no goals

Proof state:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : WeaklyLocallyCompactSpace X
f : X → Y
hf : IsOpenQuotientMap f
⊢ ∀ (x : Y), ∃ s, IsCompact s ∧ s ∈ 𝓝 x

Tactic:
refine hf.surjective.forall.2 fun x ↦ ?_

Result:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : WeaklyLocallyCompactSpace X
f : X → Y
hf : IsOpenQuotientMap f
x : X
⊢ ∃ s, IsCompact s ∧ s ∈ 𝓝 (f x)

Proof state:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : WeaklyLocallyCompactSpace X
f : X → Y
hf : IsOpenQuotientMap f
x : X
⊢ ∃ s, IsCompact s ∧ s ∈ 𝓝 (f x)

Tactic:
rcases exists_compact_mem_nhds x with ⟨K, hKc, hKx⟩

Result:
case intro.intro
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : WeaklyLocallyCompactSpace X
f : X → Y
hf : IsOpenQuotientMap f
x : X
K : Set X
hKc : IsCompact K
hKx : K ∈ 𝓝 x
⊢ ∃ s, IsCompact s ∧ s ∈ 𝓝 (f x)
-- Mathlib/Data/Finset/Lattice/Basic.lean
theorem inter_union_self (s t : Finset α) : s ∩ (t ∪ s) = s

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s t : Finset α
⊢ s ∩ (t ∪ s) = s

Tactic:
rw [inter_comm, union_inter_cancel_right]

Result:
no goals
-- Mathlib/Algebra/Module/Submodule/Map.lean
lemma comap_lt_comap_iff_of_surjective {p q : Submodule R₂ M₂} : p.comap f < q.comap f ↔ p < q

Proof state:
R : Type u_1
R₂ : Type u_3
M : Type u_5
M₂ : Type u_7
inst✝⁸ : Semiring R
inst✝⁷ : Semiring R₂
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid M₂
inst✝⁴ : Module R M
inst✝³ : Module R₂ M₂
σ₁₂ : R →+* R₂
F : Type u_9
inst✝² : FunLike F M M₂
inst✝¹ : SemilinearMapClass F σ₁₂ M M₂
inst✝ : RingHomSurjective σ₁₂
f : F
hf : Surjective ⇑f
p q : Submodule R₂ M₂
⊢ comap f p < comap f q ↔ p < q

Tactic:
apply lt_iff_lt_of_le_iff_le' <;> exact comap_le_comap_iff_of_surjective hf

Result:
no goals
-- Mathlib/Algebra/Polynomial/Degree/Definitions.lean
theorem natDegree_eq_zero_iff_degree_le_zero : p.natDegree = 0 ↔ p.degree ≤ 0

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
⊢ p.natDegree = 0 ↔ p.degree ≤ 0

Tactic:
rw [← nonpos_iff_eq_zero, natDegree_le_iff_degree_le, Nat.cast_zero]

Result:
no goals