harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Topology/MetricSpace/Dilation.lean
theorem ratio_ne_zero [DilationClass F α β] (f : F) : ratio f ≠ 0

Proof state:
case neg
α : Type u_1
β : Type u_2
F : Type u_4
inst✝³ : PseudoEMetricSpace α
inst✝² : PseudoEMetricSpace β
inst✝¹ : FunLike F α β
inst✝ : DilationClass F α β
f : F
h✝ : ¬∀ (x y : α), edist x y = 0 ∨ edist x y = ⊤
⊢ ⋯.choose ≠ 0

Tactic:
exact (DilationClass.edist_eq' f).choose_spec.1

Result:
no goals

Proof state:
case pos
α : Type u_1
β : Type u_2
F : Type u_4
inst✝³ : PseudoEMetricSpace α
inst✝² : PseudoEMetricSpace β
inst✝¹ : FunLike F α β
inst✝ : DilationClass F α β
f : F
h✝ : ∀ (x y : α), edist x y = 0 ∨ edist x y = ⊤
⊢ 1 ≠ 0

Tactic:
exact one_ne_zero

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
F : Type u_4
inst✝³ : PseudoEMetricSpace α
inst✝² : PseudoEMetricSpace β
inst✝¹ : FunLike F α β
inst✝ : DilationClass F α β
f : F
⊢ ratio f ≠ 0

Tactic:
rw [ratio]

Result:
α : Type u_1
β : Type u_2
F : Type u_4
inst✝³ : PseudoEMetricSpace α
inst✝² : PseudoEMetricSpace β
inst✝¹ : FunLike F α β
inst✝ : DilationClass F α β
f : F
⊢ (if ∀ (x y : α), edist x y = 0 ∨ edist x y = ⊤ then 1 else ⋯.choose) ≠ 0

Proof state:
α : Type u_1
β : Type u_2
F : Type u_4
inst✝³ : PseudoEMetricSpace α
inst✝² : PseudoEMetricSpace β
inst✝¹ : FunLike F α β
inst✝ : DilationClass F α β
f : F
⊢ (if ∀ (x y : α), edist x y = 0 ∨ edist x y = ⊤ then 1 else ⋯.choose) ≠ 0

Tactic:
split_ifs

Result:
case pos
α : Type u_1
β : Type u_2
F : Type u_4
inst✝³ : PseudoEMetricSpace α
inst✝² : PseudoEMetricSpace β
inst✝¹ : FunLike F α β
inst✝ : DilationClass F α β
f : F
h✝ : ∀ (x y : α), edist x y = 0 ∨ edist x y = ⊤
⊢ 1 ≠ 0

case neg
α : Type u_1
β : Type u_2
F : Type u_4
inst✝³ : PseudoEMetricSpace α
inst✝² : PseudoEMetricSpace β
inst✝¹ : FunLike F α β
inst✝ : DilationClass F α β
f : F
h✝ : ¬∀ (x y : α), edist x y = 0 ∨ edist x y = ⊤
⊢ ⋯.choose ≠ 0
-- Mathlib/Algebra/GroupWithZero/Units/Basic.lean
@[simp] lemma div_mul_div_cancel₀' (ha : a ≠ 0) (b c : G₀) : a / b * (c / a) = c / b

Proof state:
G₀ : Type u_3
inst✝ : CommGroupWithZero G₀
a : G₀
ha : a ≠ 0
b c : G₀
⊢ a / b * (c / a) = c / b

Tactic:
rw [mul_comm, div_mul_div_cancel₀ ha]

Result:
no goals
-- Mathlib/Topology/Compactness/Lindelof.lean
theorem Topology.IsClosedEmbedding.LindelofSpace [h : LindelofSpace Y] {f : X → Y}
    (hf : IsClosedEmbedding f) : LindelofSpace X :=
  ⟨by rw [hf.isInducing.isLindelof_iff, image_univ]; exact hf.isClosed_range.isLindelof⟩

Proof state:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
h : LindelofSpace Y
f : X → Y
hf : IsClosedEmbedding f
⊢ IsLindelof (range f)

Tactic:
exact hf.isClosed_range.isLindelof

Result:
no goals

Proof state:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
h : LindelofSpace Y
f : X → Y
hf : IsClosedEmbedding f
⊢ IsLindelof univ

Tactic:
rw [hf.isInducing.isLindelof_iff, image_univ]

Result:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
h : LindelofSpace Y
f : X → Y
hf : IsClosedEmbedding f
⊢ IsLindelof (range f)
-- Mathlib/RingTheory/FinitePresentation.lean
theorem trans [Algebra A B] [IsScalarTower R A B] [FinitePresentation R A]
    [FinitePresentation A B] : FinitePresentation R B

Proof state:
R : Type w₁
A : Type w₂
B : Type w₃
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra R B
inst✝³ : Algebra A B
inst✝² : IsScalarTower R A B
inst✝¹ : FinitePresentation R A
inst✝ : FinitePresentation A B
⊢ FinitePresentation R B

Tactic:
have hfpB : FinitePresentation A B := inferInstance

Result:
R : Type w₁
A : Type w₂
B : Type w₃
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra R B
inst✝³ : Algebra A B
inst✝² : IsScalarTower R A B
inst✝¹ : FinitePresentation R A
inst✝ hfpB : FinitePresentation A B
⊢ FinitePresentation R B

Proof state:
R : Type w₁
A : Type w₂
B : Type w₃
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra R B
inst✝³ : Algebra A B
inst✝² : IsScalarTower R A B
inst✝¹ : FinitePresentation R A
inst✝ hfpB : FinitePresentation A B
⊢ FinitePresentation R B

Tactic:
obtain ⟨n, I, e, hfg⟩ := iff.1 hfpB

Result:
case intro.intro.intro
R : Type w₁
A : Type w₂
B : Type w₃
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra R B
inst✝³ : Algebra A B
inst✝² : IsScalarTower R A B
inst✝¹ : FinitePresentation R A
inst✝ hfpB : FinitePresentation A B
n : ℕ
I : Ideal (MvPolynomial (Fin n) A)
e : (MvPolynomial (Fin n) A ⧸ I) ≃ₐ[A] B
hfg : I.FG
⊢ FinitePresentation R B

Proof state:
case intro.intro.intro
R : Type w₁
A : Type w₂
B : Type w₃
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra R B
inst✝³ : Algebra A B
inst✝² : IsScalarTower R A B
inst✝¹ : FinitePresentation R A
inst✝ hfpB : FinitePresentation A B
n : ℕ
I : Ideal (MvPolynomial (Fin n) A)
e : (MvPolynomial (Fin n) A ⧸ I) ≃ₐ[A] B
hfg : I.FG
this : FinitePresentation R (MvPolynomial (Fin n) A ⧸ I) := FinitePresentation.quotient hfg
⊢ FinitePresentation R B

Tactic:
exact equiv (e.restrictScalars R)

Result:
no goals

Proof state:
case intro.intro.intro
R : Type w₁
A : Type w₂
B : Type w₃
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra R B
inst✝³ : Algebra A B
inst✝² : IsScalarTower R A B
inst✝¹ : FinitePresentation R A
inst✝ hfpB : FinitePresentation A B
n : ℕ
I : Ideal (MvPolynomial (Fin n) A)
e : (MvPolynomial (Fin n) A ⧸ I) ≃ₐ[A] B
hfg : I.FG
⊢ FinitePresentation R B

Tactic:
letI : FinitePresentation R (MvPolynomial (Fin n) A ⧸ I) :=
  (mvPolynomial_of_finitePresentation _).quotient hfg

Result:
case intro.intro.intro
R : Type w₁
A : Type w₂
B : Type w₃
inst✝⁸ : CommRing R
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
inst✝⁵ : CommRing B
inst✝⁴ : Algebra R B
inst✝³ : Algebra A B
inst✝² : IsScalarTower R A B
inst✝¹ : FinitePresentation R A
inst✝ hfpB : FinitePresentation A B
n : ℕ
I : Ideal (MvPolynomial (Fin n) A)
e : (MvPolynomial (Fin n) A ⧸ I) ≃ₐ[A] B
hfg : I.FG
this : FinitePresentation R (MvPolynomial (Fin n) A ⧸ I) := FinitePresentation.quotient hfg
⊢ FinitePresentation R B
-- Mathlib/Order/Interval/Finset/Fin.lean
theorem map_valEmbedding_Ioo : (Ioo a b).map Fin.valEmbedding = Ioo ↑a ↑b

Proof state:
n : ℕ
a b : Fin n
⊢ map valEmbedding (Ioo a b) = Ioo ↑a ↑b

Tactic:
simp [Ioo_eq_finset_subtype, Finset.fin, Finset.map_map]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/SesquilinearForm.lean
theorem LinearMap.toMatrix₂'_compl₂ (B : (n → R) →ₗ[R] (m → R) →ₗ[R] R) (f : (m' → R) →ₗ[R] m → R) :
    toMatrix₂' R (B.compl₂ f) = toMatrix₂' R B * toMatrix' f

Proof state:
n : Type u_11
m : Type u_12
m' : Type u_14
R : Type u_16
inst✝⁶ : CommSemiring R
inst✝⁵ : Fintype n
inst✝⁴ : Fintype m
inst✝³ : DecidableEq n
inst✝² : DecidableEq m
inst✝¹ : Fintype m'
inst✝ : DecidableEq m'
B : (n → R) →ₗ[R] (m → R) →ₗ[R] R
f : (m' → R) →ₗ[R] m → R
⊢ (toMatrix₂' R) (B.compl₂ f) = (toMatrix₂' R) B * toMatrix' f

Tactic:
rw [← LinearMap.comp_id B, ← LinearMap.compl₁₂]

Result:
n : Type u_11
m : Type u_12
m' : Type u_14
R : Type u_16
inst✝⁶ : CommSemiring R
inst✝⁵ : Fintype n
inst✝⁴ : Fintype m
inst✝³ : DecidableEq n
inst✝² : DecidableEq m
inst✝¹ : Fintype m'
inst✝ : DecidableEq m'
B : (n → R) →ₗ[R] (m → R) →ₗ[R] R
f : (m' → R) →ₗ[R] m → R
⊢ (toMatrix₂' R) (B.compl₁₂ id f) = (toMatrix₂' R) (B ∘ₗ id) * toMatrix' f

Proof state:
n : Type u_11
m : Type u_12
m' : Type u_14
R : Type u_16
inst✝⁶ : CommSemiring R
inst✝⁵ : Fintype n
inst✝⁴ : Fintype m
inst✝³ : DecidableEq n
inst✝² : DecidableEq m
inst✝¹ : Fintype m'
inst✝ : DecidableEq m'
B : (n → R) →ₗ[R] (m → R) →ₗ[R] R
f : (m' → R) →ₗ[R] m → R
⊢ (toMatrix₂' R) (B.compl₁₂ id f) = (toMatrix₂' R) (B ∘ₗ id) * toMatrix' f

Tactic:
simp

Result:
no goals
-- Mathlib/Topology/MetricSpace/Defs.lean
theorem zero_eq_dist {x y : γ} : 0 = dist x y ↔ x = y

Proof state:
γ : Type w
inst✝ : MetricSpace γ
x y : γ
⊢ 0 = dist x y ↔ x = y

Tactic:
rw [eq_comm, dist_eq_zero]

Result:
no goals
-- Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean
theorem posMulReflectLT_iff_mulPosReflectLT : PosMulReflectLT α ↔ MulPosReflectLT α

Proof state:
α : Type u_3
inst✝³ : Mul α
inst✝² : Std.Commutative fun x1 x2 => x1 * x2
inst✝¹ : Zero α
inst✝ : Preorder α
⊢ PosMulReflectLT α ↔ MulPosReflectLT α

Tactic:
simp only [posMulReflectLT_iff, mulPosReflectLT_iff, Std.Commutative.comm]

Result:
no goals
-- Mathlib/Topology/Germ.lean
theorem eq_of_germ_isConstant [i : PreconnectedSpace X]
    (h : ∀ x : X, (f : Germ (𝓝 x) Y).IsConstant) (x x' : X) : f x = f x' :=
  (IsLocallyConstant.of_germ_isConstant h).apply_eq_of_isPreconnected
    (preconnectedSpace_iff_univ.mp i) (by trivial) (by trivial)

Proof state:
X : Type u_1
Y : Type u_2
inst✝ : TopologicalSpace X
f : X → Y
i : PreconnectedSpace X
h : ∀ (x : X), (↑f).IsConstant
x x' : X
⊢ x' ∈ univ

Tactic:
trivial

Result:
no goals

Proof state:
X : Type u_1
Y : Type u_2
inst✝ : TopologicalSpace X
f : X → Y
i : PreconnectedSpace X
h : ∀ (x : X), (↑f).IsConstant
x x' : X
⊢ x ∈ univ

Tactic:
trivial

Result:
no goals
-- Mathlib/NumberTheory/Cyclotomic/Rat.lean
theorem integralPowerBasis_dim [hcycl : IsCyclotomicExtension {p ^ k} ℚ K]
    (hζ : IsPrimitiveRoot ζ ↑(p ^ k)) : hζ.integralPowerBasis.dim = φ (p ^ k)

Proof state:
p : ℕ+
k : ℕ
K : Type u
inst✝¹ : Field K
ζ : K
hp : Fact (Nat.Prime ↑p)
inst✝ : CharZero K
hcycl : IsCyclotomicExtension {p ^ k} ℚ K
hζ : IsPrimitiveRoot ζ ↑(p ^ k)
⊢ hζ.integralPowerBasis.dim = φ (↑p ^ k)

Tactic:
simp [integralPowerBasis, ← cyclotomic_eq_minpoly hζ, natDegree_cyclotomic]

Result:
no goals
-- Mathlib/Algebra/Ring/BooleanRing.lean
theorem inf_comm (a b : α) : a ⊓ b = b ⊓ a

Proof state:
α : Type u_1
inst✝ : BooleanRing α
a b : α
⊢ a * b = b * a

Tactic:
ring

Result:
no goals
-- Mathlib/GroupTheory/FreeAbelianGroupFinsupp.lean
theorem support_of (x : X) : support (of x) = {x}

Proof state:
X : Type u_1
x : X
⊢ (of x).support = {x}

Tactic:
rw [support, toFinsupp_of, Finsupp.support_single_ne_zero _ one_ne_zero]

Result:
no goals
-- Mathlib/Algebra/Ring/Subsemiring/MulOpposite.lean
theorem unop_closure (s : Set Rᵐᵒᵖ) : (closure s).unop = closure (MulOpposite.op ⁻¹' s)

Proof state:
R : Type u_2
inst✝ : NonAssocSemiring R
s : Set Rᵐᵒᵖ
⊢ (closure s).unop = closure (MulOpposite.op ⁻¹' s)

Tactic:
rw [← op_inj, op_unop, op_closure]

Result:
R : Type u_2
inst✝ : NonAssocSemiring R
s : Set Rᵐᵒᵖ
⊢ closure s = closure (MulOpposite.unop ⁻¹' (MulOpposite.op ⁻¹' s))

Proof state:
R : Type u_2
inst✝ : NonAssocSemiring R
s : Set Rᵐᵒᵖ
⊢ closure s = closure (MulOpposite.unop ⁻¹' (MulOpposite.op ⁻¹' s))

Tactic:
simp_rw [Set.preimage_preimage, MulOpposite.op_unop, Set.preimage_id']

Result:
no goals
-- Mathlib/Topology/UniformSpace/UniformConvergence.lean
theorem tendstoLocallyUniformly_iff_filter :
    TendstoLocallyUniformly F f p ↔ ∀ x, TendstoUniformlyOnFilter F f p (𝓝 x)

Proof state:
α : Type u
β : Type v
ι : Type x
inst✝¹ : UniformSpace β
F : ι → α → β
f : α → β
p : Filter ι
inst✝ : TopologicalSpace α
⊢ TendstoLocallyUniformly F f p ↔ ∀ (x : α), TendstoUniformlyOnFilter F f p (𝓝 x)

Tactic:
simpa [← tendstoLocallyUniformlyOn_univ, ← nhdsWithin_univ] using
  @tendstoLocallyUniformlyOn_iff_filter _ _ _ _ F f univ p _

Result:
no goals
-- Mathlib/Analysis/Calculus/Deriv/Basic.lean
theorem norm_deriv_le_of_lipschitz {f : 𝕜 → F} {x₀ : 𝕜}
    {C : ℝ≥0} (hlip : LipschitzWith C f) : ‖deriv f x₀‖ ≤ C

Proof state:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
x₀ : 𝕜
C : ℝ≥0
hlip : LipschitzWith C f
⊢ ‖deriv f x₀‖ ≤ ↑C

Tactic:
simpa [norm_deriv_eq_norm_fderiv] using norm_fderiv_le_of_lipschitz 𝕜 hlip

Result:
no goals
-- Mathlib/Data/ULift.lean
theorem up_inj {x y : α} : up x = up y ↔ x = y

Proof state:
α : Type u
x y : α
⊢ { down := x } = { down := y } ↔ x = y

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Algebra/NonUnitalHom.lean
theorem coe_distribMulActionHom_mk (f : A →ₛₙₐ[φ] B) (h₁ h₂ h₃ h₄) :
    ((⟨⟨⟨f, h₁⟩, h₂, h₃⟩, h₄⟩ : A →ₛₙₐ[φ] B) : A →ₑ+[φ] B) = ⟨⟨f, h₁⟩, h₂, h₃⟩

Proof state:
R : Type u
S : Type u₁
inst✝⁵ : Monoid R
inst✝⁴ : Monoid S
φ : R →* S
A : Type v
B : Type w
inst✝³ : NonUnitalNonAssocSemiring A
inst✝² : DistribMulAction R A
inst✝¹ : NonUnitalNonAssocSemiring B
inst✝ : DistribMulAction S B
f : A →ₛₙₐ[φ] B
h₁ : ∀ (m : R) (x : A), f (m • x) = φ m • f x
h₂ : { toFun := ⇑f, map_smul' := h₁ }.toFun 0 = 0
h₃ :
  ∀ (x y : A),
    { toFun := ⇑f, map_smul' := h₁ }.toFun (x + y) =
      { toFun := ⇑f, map_smul' := h₁ }.toFun x + { toFun := ⇑f, map_smul' := h₁ }.toFun y
h₄ :
  ∀ (x y : A),
    { toFun := ⇑f, map_smul' := h₁, map_zero' := h₂, map_add' := h₃ }.toFun (x * y) =
      { toFun := ⇑f, map_smul' := h₁, map_zero' := h₂, map_add' := h₃ }.toFun x *
        { toFun := ⇑f, map_smul' := h₁, map_zero' := h₂, map_add' := h₃ }.toFun y
⊢ ↑{ toFun := ⇑f, map_smul' := h₁, map_zero' := h₂, map_add' := h₃, map_mul' := h₄ } =
    { toFun := ⇑f, map_smul' := h₁, map_zero' := h₂, map_add' := h₃ }

Tactic:
rfl

Result:
no goals
-- Mathlib/Topology/UniformSpace/Equicontinuity.lean
theorem equicontinuousAt_iff_range {F : ι → X → α} {x₀ : X} :
    EquicontinuousAt F x₀ ↔ EquicontinuousAt ((↑) : range F → X → α) x₀

Proof state:
ι : Type u_1
X : Type u_3
α : Type u_6
tX : TopologicalSpace X
uα : UniformSpace α
F : ι → X → α
x₀ : X
⊢ EquicontinuousAt F x₀ ↔ EquicontinuousAt Subtype.val x₀

Tactic:
simp only [EquicontinuousAt, forall_subtype_range_iff]

Result:
no goals
-- Mathlib/Analysis/Normed/Group/Pointwise.lean
theorem ball_one_mul_singleton : ball 1 δ * {x} = ball x δ

Proof state:
E : Type u_1
inst✝ : SeminormedCommGroup E
δ : ℝ
x : E
⊢ ball 1 δ * {x} = ball x δ

Tactic:
simp [ball_mul_singleton]

Result:
no goals
-- Mathlib/Analysis/Calculus/Deriv/Basic.lean
theorem derivWithin_zero_of_isolated (h : 𝓝[s \ {x}] x = ⊥) : derivWithin f s x = 0

Proof state:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
x : 𝕜
s : Set 𝕜
h : 𝓝[s \ {x}] x = ⊥
⊢ derivWithin f s x = 0

Tactic:
rw [derivWithin, fderivWithin_zero_of_isolated h, ContinuousLinearMap.zero_apply]

Result:
no goals
-- Mathlib/AlgebraicTopology/SimplicialSet/Nerve.lean
theorem δ₂_mk₂_eq : (nerve C).δ 2 (ComposableArrows.mk₂ f g) = ComposableArrows.mk₁ f :=
  ComposableArrows.ext₁ rfl rfl (by simp; rfl)

Proof state:
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X₀ X₁ X₂ : C
f : X₀ ⟶ X₁
g : X₁ ⟶ X₂
⊢ ComposableArrows.hom (SimplicialObject.δ (nerve C) 2 (ComposableArrows.mk₂ f g)) =
    eqToHom ⋯ ≫ (ComposableArrows.mk₁ f).hom ≫ eqToHom ⋯

Tactic:
simp

Result:
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X₀ X₁ X₂ : C
f : X₀ ⟶ X₁
g : X₁ ⟶ X₂
⊢ ComposableArrows.hom (SimplicialObject.δ (nerve C) 2 ((ComposableArrows.mk₁ g).precomp f)) = f

Proof state:
C : Type u_1
inst✝ : Category.{u_2, u_1} C
X₀ X₁ X₂ : C
f : X₀ ⟶ X₁
g : X₁ ⟶ X₂
⊢ ComposableArrows.hom (SimplicialObject.δ (nerve C) 2 ((ComposableArrows.mk₁ g).precomp f)) = f

Tactic:
rfl

Result:
no goals
-- Mathlib/Data/Real/Irrational.lean
theorem irrational_nat_mul_iff : Irrational (n * x) ↔ n ≠ 0 ∧ Irrational x

Proof state:
n : ℕ
x : ℝ
⊢ Irrational (↑n * x) ↔ n ≠ 0 ∧ Irrational x

Tactic:
rw [← cast_natCast, irrational_rat_mul_iff, Nat.cast_ne_zero]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/SetToL1.lean
theorem setToFun_zero (hT : DominatedFinMeasAdditive μ T C) : setToFun μ T hT (0 : α → E) = 0

Proof state:
α : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NormedAddCommGroup E
inst✝³ : NormedSpace ℝ E
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace ℝ F
m : MeasurableSpace α
μ : Measure α
inst✝ : CompleteSpace F
T : Set α → E →L[ℝ] F
C : ℝ
hT : DominatedFinMeasAdditive μ T C
⊢ setToFun μ T hT 0 = 0

Tactic:
erw [setToFun_eq hT (integrable_zero _ _ _), Integrable.toL1_zero, ContinuousLinearMap.map_zero]

Result:
no goals
-- Mathlib/Algebra/MvPolynomial/Eval.lean
theorem eval₂_C (a) : (C a).eval₂ f g = f a

Proof state:
R : Type u
S₁ : Type v
σ : Type u_1
inst✝¹ : CommSemiring R
inst✝ : CommSemiring S₁
f : R →+* S₁
g : σ → S₁
a : R
⊢ eval₂ f g (C a) = f a

Tactic:
rw [C_apply, eval₂_monomial, prod_zero_index, mul_one]

Result:
no goals
-- Mathlib/Algebra/Category/Grp/Basic.lean
@[to_additive]
lemma inv_hom_apply {X Y : Grp} (e : X ≅ Y) (x : X) : e.inv (e.hom x) = x

Proof state:
X Y : Grp
e : X ≅ Y
x : ↑X
⊢ (ConcreteCategory.hom e.inv) ((ConcreteCategory.hom e.hom) x) = x

Tactic:
simp

Result:
no goals
-- Mathlib/CategoryTheory/Monoidal/Cartesian/Mon_.lean
theorem lift_comp_one_left {A : C} {B : Mon_ C} (f : A ⟶ 𝟙_ C) (g : A ⟶ B.X) :
    lift (f ≫ B.one) g ≫ B.mul = g

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : ChosenFiniteProducts C
A : C
B : Mon_ C
f : A ⟶ 𝟙_ C
g : A ⟶ B.X
⊢ lift (f ≫ B.one) g ≫ B.mul = g

Tactic:
have := lift f g ≫= B.one_mul

Result:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : ChosenFiniteProducts C
A : C
B : Mon_ C
f : A ⟶ 𝟙_ C
g : A ⟶ B.X
this : lift f g ≫ B.one ▷ B.X ≫ B.mul = lift f g ≫ (λ_ B.X).hom
⊢ lift (f ≫ B.one) g ≫ B.mul = g

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
inst✝ : ChosenFiniteProducts C
A : C
B : Mon_ C
f : A ⟶ 𝟙_ C
g : A ⟶ B.X
this : lift f g ≫ B.one ▷ B.X ≫ B.mul = lift f g ≫ (λ_ B.X).hom
⊢ lift (f ≫ B.one) g ≫ B.mul = g

Tactic:
rwa [lift_whiskerRight_assoc, lift_leftUnitor_hom] at this

Result:
no goals
-- Mathlib/Data/DFinsupp/Defs.lean
theorem filter_apply_neg [∀ i, Zero (β i)] {p : ι → Prop} [DecidablePred p] (f : Π₀ i, β i) {i : ι}
    (h : ¬p i) : f.filter p i = 0

Proof state:
ι : Type u
β : ι → Type v
inst✝¹ : (i : ι) → Zero (β i)
p : ι → Prop
inst✝ : DecidablePred p
f : Π₀ (i : ι), β i
i : ι
h : ¬p i
⊢ (filter p f) i = 0

Tactic:
simp only [filter_apply, if_neg h]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/Circulant.lean
theorem circulant_single (n) [Semiring α] [DecidableEq n] [AddGroup n] [Fintype n] (a : α) :
    circulant (Pi.single 0 a : n → α) = scalar n a

Proof state:
case a
α : Type u_1
n : Type u_5
inst✝³ : Semiring α
inst✝² : DecidableEq n
inst✝¹ : AddGroup n
inst✝ : Fintype n
a : α
i j : n
⊢ circulant (Pi.single 0 a) i j = (scalar n) a i j

Tactic:
simp [Pi.single_apply, diagonal_apply, sub_eq_zero]

Result:
no goals

Proof state:
α : Type u_1
n : Type u_5
inst✝³ : Semiring α
inst✝² : DecidableEq n
inst✝¹ : AddGroup n
inst✝ : Fintype n
a : α
⊢ circulant (Pi.single 0 a) = (scalar n) a

Tactic:
ext i j

Result:
case a
α : Type u_1
n : Type u_5
inst✝³ : Semiring α
inst✝² : DecidableEq n
inst✝¹ : AddGroup n
inst✝ : Fintype n
a : α
i j : n
⊢ circulant (Pi.single 0 a) i j = (scalar n) a i j
-- Mathlib/AlgebraicGeometry/PullbackCarrier.lean
/-- Given a triple `(x, y, s)` with `f x = s = f y` there exists `t : X ×[S] Y` above
`x` and `ỳ`. For the unpacked version without `Triplet`, see
`AlgebraicGeometry.Scheme.Pullback.exists_preimage`. -/
lemma Triplet.exists_preimage (T : Triplet f g) :
    ∃ t : ↑(pullback f g),
    (pullback.fst f g).base t = T.x ∧ (pullback.snd f g).base t = T.y :=
  ⟨carrierEquiv.symm ⟨T, Nonempty.some inferInstance⟩, by simp⟩

Proof state:
X Y S : Scheme
f : X ⟶ S
g : Y ⟶ S
T : Triplet f g
⊢ (ConcreteCategory.hom (pullback.fst f g).base) (carrierEquiv.symm ⟨T, ⋯.some⟩) = T.x ∧
    (ConcreteCategory.hom (pullback.snd f g).base) (carrierEquiv.symm ⟨T, ⋯.some⟩) = T.y

Tactic:
simp

Result:
no goals
-- Mathlib/RingTheory/Ideal/Prod.lean
theorem prod_top_top : prod (⊤ : Ideal R) (⊤ : Ideal S) = ⊤ :=
  Ideal.ext <| by simp

Proof state:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
⊢ ∀ (x : R × S), x ∈ ⊤.prod ⊤ ↔ x ∈ ⊤

Tactic:
simp

Result:
no goals
-- Mathlib/Order/Interval/Set/Basic.lean
theorem left_mem_Ioo : a ∈ Ioo a b ↔ False

Proof state:
α : Type u_1
inst✝ : Preorder α
a b : α
⊢ a ∈ Ioo a b ↔ False

Tactic:
simp [lt_irrefl]

Result:
no goals
-- Mathlib/Data/Complex/Trigonometric.lean
theorem cot_eq_cos_div_sin : cot x = cos x / sin x :=
  ofReal_injective <| by simp [cot_eq_cos_div_sin]

Proof state:
x : ℝ
⊢ ↑x.cot = ↑(cos x / sin x)

Tactic:
simp [cot_eq_cos_div_sin]

Result:
no goals
-- Mathlib/Topology/ContinuousOn.lean
theorem continuousWithinAt_inter (h : t ∈ 𝓝 x) :
    ContinuousWithinAt f (s ∩ t) x ↔ ContinuousWithinAt f s x

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s t : Set α
x : α
h : t ∈ 𝓝 x
⊢ ContinuousWithinAt f (s ∩ t) x ↔ ContinuousWithinAt f s x

Tactic:
simp [ContinuousWithinAt, nhdsWithin_restrict' s h]

Result:
no goals
-- Mathlib/Data/Matrix/Defs.lean
theorem dite_apply (P : Prop) [Decidable P]
    (A : P → Matrix m n α) (B : ¬P → Matrix m n α) (i : m) (j : n) :
    dite P A B i j = dite P (A · i j) (B · i j)

Proof state:
m : Type u_2
n : Type u_3
α : Type v
P : Prop
inst✝ : Decidable P
A : P → Matrix m n α
B : ¬P → Matrix m n α
i : m
j : n
⊢ dite P A B i j = if x : P then A x i j else B x i j

Tactic:
rw [dite_apply, dite_apply]

Result:
no goals
-- Mathlib/Algebra/Group/Units/Basic.lean
@[to_additive]
protected lemma mul_div_cancel (h : IsUnit a) (b : α) : a * (b / a) = b

Proof state:
α : Type u
inst✝ : DivisionCommMonoid α
a : α
h : IsUnit a
b : α
⊢ a * (b / a) = b

Tactic:
rw [mul_comm, h.div_mul_cancel]

Result:
no goals
-- Mathlib/Algebra/GCDMonoid/Basic.lean
theorem normUnit_mul_normUnit (a : α) : normUnit (a * normUnit a) = 1

Proof state:
case inr
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizationMonoid α
a : α
a✝ : Nontrivial α
h : a ≠ 0
⊢ normUnit (a * ↑(normUnit a)) = 1

Tactic:
rw [normUnit_mul h (Units.ne_zero _), normUnit_coe_units, mul_inv_eq_one]

Result:
no goals

Proof state:
case inl
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizationMonoid α
a✝ : Nontrivial α
⊢ normUnit (0 * ↑(normUnit 0)) = 1

Tactic:
rw [normUnit_zero, zero_mul, normUnit_zero]

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizationMonoid α
a : α
⊢ normUnit (a * ↑(normUnit a)) = 1

Tactic:
nontriviality α using Subsingleton.elim a 0

Result:
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizationMonoid α
a : α
a✝ : Nontrivial α
⊢ normUnit (a * ↑(normUnit a)) = 1

Proof state:
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizationMonoid α
a : α
a✝ : Nontrivial α
⊢ normUnit (a * ↑(normUnit a)) = 1

Tactic:
obtain rfl | h := eq_or_ne a 0

Result:
case inl
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizationMonoid α
a✝ : Nontrivial α
⊢ normUnit (0 * ↑(normUnit 0)) = 1

case inr
α : Type u_1
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizationMonoid α
a : α
a✝ : Nontrivial α
h : a ≠ 0
⊢ normUnit (a * ↑(normUnit a)) = 1
-- Mathlib/CategoryTheory/EffectiveEpi/Extensive.lean
theorem effectiveEpi_desc_iff_effectiveEpiFamily {α : Type} [Finite α]
    {B : C} (X : α → C) (π : (a : α) → X a ⟶ B) :
    EffectiveEpi (Sigma.desc π) ↔ EffectiveEpiFamily X π

Proof state:
C : Type u_1
inst✝² : Category.{u_2, u_1} C
inst✝¹ : FinitaryPreExtensive C
α : Type
inst✝ : Finite α
B : C
X : α → C
π : (a : α) → X a ⟶ B
⊢ EffectiveEpi (Sigma.desc π) ↔ EffectiveEpiFamily X π

Tactic:
exact ⟨fun h ↦ ⟨⟨@effectiveEpiFamilyStructOfEffectiveEpiDesc _ _ _ _ X π _ h _ _ (fun g ↦
  (FinitaryPreExtensive.sigma_desc_iso (fun a ↦ Sigma.ι X a) g inferInstance).epi_of_iso)⟩⟩,
  fun _ ↦ inferInstance⟩

Result:
no goals
-- Mathlib/Geometry/Manifold/BumpFunction.lean
theorem support_updateRIn {r : ℝ} (hr : r ∈ Ioo 0 f.rOut) :
    support (f.updateRIn r hr) = support f

Proof state:
E : Type uE
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace ℝ E
H : Type uH
inst✝³ : TopologicalSpace H
I : ModelWithCorners ℝ E H
M : Type uM
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
c : M
f : SmoothBumpFunction I c
inst✝ : FiniteDimensional ℝ E
r : ℝ
hr : r ∈ Ioo 0 f.rOut
⊢ support ↑(f.updateRIn r hr) = support ↑f

Tactic:
simp only [support_eq_inter_preimage, updateRIn_rOut]

Result:
no goals