harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Topology/Category/TopCat/Limits/Pullbacks.lean
theorem pullbackIsoProdSubtype_inv_fst (f : X ⟶ Z) (g : Y ⟶ Z) :
    (pullbackIsoProdSubtype f g).inv ≫ pullback.fst _ _ = pullbackFst f g

Proof state:
X Y Z : TopCat
f : X ⟶ Z
g : Y ⟶ Z
⊢ (pullbackIsoProdSubtype f g).inv ≫ pullback.fst f g = pullbackFst f g

Tactic:
simp [pullbackCone, pullbackIsoProdSubtype]

Result:
no goals
-- Mathlib/Data/Nat/Bitwise.lean
theorem testBit_eq_false_of_lt {n i} (h : n < 2 ^ i) : n.testBit i = false

Proof state:
n i : ℕ
h : n < 2 ^ i
⊢ n.testBit i = false

Tactic:
simp [testBit, shiftRight_eq_div_pow, Nat.div_eq_of_lt h]

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Unoriented/Basic.lean
theorem cos_eq_zero_iff_angle_eq_pi_div_two : cos (angle x y) = 0 ↔ angle x y = π / 2

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
⊢ π / 2 ∈ Icc 0 π

Tactic:
constructor <;> linarith [pi_pos]

Result:
no goals

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
⊢ cos (angle x y) = 0 ↔ angle x y = π / 2

Tactic:
rw [← cos_pi_div_two]

Result:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
⊢ cos (angle x y) = cos (π / 2) ↔ angle x y = π / 2

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
⊢ cos (angle x y) = cos (π / 2) ↔ angle x y = π / 2

Tactic:
apply injOn_cos.eq_iff ⟨angle_nonneg x y, angle_le_pi x y⟩

Result:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
⊢ π / 2 ∈ Icc 0 π
-- Mathlib/Analysis/Normed/Group/Basic.lean
theorem mem_emetric_ball_one_iff {r : ℝ≥0∞} : a ∈ EMetric.ball 1 r ↔ ‖a‖ₑ < r

Proof state:
E : Type u_5
inst✝ : SeminormedGroup E
a : E
r : ℝ≥0∞
⊢ a ∈ EMetric.ball 1 r ↔ ‖a‖ₑ < r

Tactic:
rw [EMetric.mem_ball, edist_one_eq_enorm]

Result:
no goals
-- Mathlib/AlgebraicTopology/TopologicalSimplex.lean
@[simp]
lemma toTopObj_zero_apply_zero (f : ⦋0⦌.toTopObj) : f 0 = 1

Proof state:
f : ↑⦋0⦌.toTopObj
⊢ ↑f 0 = 1

Tactic:
simpa [toType_apply] using show ∑ _, _ = _ from f.2

Result:
no goals
-- Mathlib/Computability/DFA.lean
theorem mem_accepts {x : List α} : x ∈ M.accepts ↔ M.eval x ∈ M.accept

Proof state:
α : Type u
σ : Type v
M : DFA α σ
x : List α
⊢ x ∈ M.accepts ↔ M.eval x ∈ M.accept

Tactic:
rfl

Result:
no goals
-- Mathlib/LinearAlgebra/Prod.lean
theorem ker_prod (f : M →ₗ[R] M₂) (g : M →ₗ[R] M₃) : ker (prod f g) = ker f ⊓ ker g

Proof state:
R : Type u
M : Type v
M₂ : Type w
M₃ : Type y
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M₂
inst✝³ : AddCommMonoid M₃
inst✝² : Module R M
inst✝¹ : Module R M₂
inst✝ : Module R M₃
f : M →ₗ[R] M₂
g : M →ₗ[R] M₃
⊢ comap f ⊥ ⊓ comap g ⊥ = ker f ⊓ ker g

Tactic:
rfl

Result:
no goals

Proof state:
R : Type u
M : Type v
M₂ : Type w
M₃ : Type y
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M₂
inst✝³ : AddCommMonoid M₃
inst✝² : Module R M
inst✝¹ : Module R M₂
inst✝ : Module R M₃
f : M →ₗ[R] M₂
g : M →ₗ[R] M₃
⊢ ker (f.prod g) = ker f ⊓ ker g

Tactic:
rw [ker, ← prod_bot, comap_prod_prod]

Result:
R : Type u
M : Type v
M₂ : Type w
M₃ : Type y
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M₂
inst✝³ : AddCommMonoid M₃
inst✝² : Module R M
inst✝¹ : Module R M₂
inst✝ : Module R M₃
f : M →ₗ[R] M₂
g : M →ₗ[R] M₃
⊢ comap f ⊥ ⊓ comap g ⊥ = ker f ⊓ ker g
-- Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean
theorem eLpNorm_exponent_zero {f : α → ε} : eLpNorm f 0 μ = 0

Proof state:
α : Type u_1
ε : Type u_2
m0 : MeasurableSpace α
μ : Measure α
inst✝ : ENorm ε
f : α → ε
⊢ eLpNorm f 0 μ = 0

Tactic:
simp [eLpNorm]

Result:
no goals
-- Mathlib/Algebra/Homology/ShortComplex/RightHomology.lean
lemma rightHomologyMap_comm [S₁.HasRightHomology] [S₂.HasRightHomology] :
    rightHomologyMap φ ≫ h₂.rightHomologyIso.hom = h₁.rightHomologyIso.hom ≫ γ.φH

Proof state:
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : HasZeroMorphisms C
S₁ S₂ : ShortComplex C
φ : S₁ ⟶ S₂
h₁ : S₁.RightHomologyData
h₂ : S₂.RightHomologyData
γ : RightHomologyMapData φ h₁ h₂
inst✝¹ : S₁.HasRightHomology
inst✝ : S₂.HasRightHomology
⊢ rightHomologyMap φ ≫ h₂.rightHomologyIso.hom = h₁.rightHomologyIso.hom ≫ γ.φH

Tactic:
simp only [γ.rightHomologyMap_eq, assoc, Iso.inv_hom_id, comp_id]

Result:
no goals
-- Mathlib/LinearAlgebra/ExteriorAlgebra/Basic.lean
/-- For a linear map `f` from `M` to `N`,
`ExteriorAlgebra.map g` is a retraction of `ExteriorAlgebra.map f` iff
`g` is a retraction of `f`. -/
@[simp]
lemma leftInverse_map_iff {f : M →ₗ[R] N} {g : N →ₗ[R] M} :
    LeftInverse (map g) (map f) ↔ LeftInverse g f

Proof state:
R : Type u1
inst✝⁴ : CommRing R
M : Type u2
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u4
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₗ[R] N
g : N →ₗ[R] M
h : LeftInverse ⇑(map g) ⇑(map f)
x : M
⊢ g (f x) = x

Tactic:
simpa using h (ι _ x)

Result:
no goals

Proof state:
R : Type u1
inst✝⁴ : CommRing R
M : Type u2
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u4
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₗ[R] N
g : N →ₗ[R] M
⊢ LeftInverse ⇑(map g) ⇑(map f) ↔ LeftInverse ⇑g ⇑f

Tactic:
refine ⟨fun h x => ?_, fun h => CliffordAlgebra.leftInverse_map_of_leftInverse _ _ h⟩

Result:
R : Type u1
inst✝⁴ : CommRing R
M : Type u2
inst✝³ : AddCommGroup M
inst✝² : Module R M
N : Type u4
inst✝¹ : AddCommGroup N
inst✝ : Module R N
f : M →ₗ[R] N
g : N →ₗ[R] M
h : LeftInverse ⇑(map g) ⇑(map f)
x : M
⊢ g (f x) = x
-- Mathlib/Topology/ContinuousOn.lean
theorem continuousWithinAt_congr_set (h : s =ᶠ[𝓝 x] t) :
    ContinuousWithinAt f s x ↔ ContinuousWithinAt f t x

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : TopologicalSpace α
inst✝ : TopologicalSpace β
f : α → β
s t : Set α
x : α
h : s =ᶠ[𝓝 x] t
⊢ ContinuousWithinAt f s x ↔ ContinuousWithinAt f t x

Tactic:
simp only [ContinuousWithinAt, nhdsWithin_eq_iff_eventuallyEq.mpr h]

Result:
no goals
-- Mathlib/Analysis/Normed/Group/Uniform.lean
@[to_additive]
lemma LocallyLipschitz.mul (hf : LocallyLipschitz f) (hg : LocallyLipschitz g) :
    LocallyLipschitz fun x ↦ f x * g x

Proof state:
α : Type u_4
E : Type u_5
inst✝¹ : SeminormedCommGroup E
inst✝ : PseudoEMetricSpace α
f g : α → E
hf : LocallyLipschitz f
hg : LocallyLipschitz g
⊢ LocallyLipschitz fun x => f x * g x

Tactic:
simpa [← locallyLipschitzOn_univ] using hf.locallyLipschitzOn.mul hg.locallyLipschitzOn

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Integrals.lean
theorem intervalIntegrable_inv (h : ∀ x : ℝ, x ∈ [[a, b]] → f x ≠ 0)
    (hf : ContinuousOn f [[a, b]]) : IntervalIntegrable (fun x => (f x)⁻¹) μ a b

Proof state:
a b : ℝ
f : ℝ → ℝ
μ : Measure ℝ
inst✝ : IsLocallyFiniteMeasure μ
h : ∀ x ∈ [[a, b]], f x ≠ 0
hf : ContinuousOn f [[a, b]]
⊢ IntervalIntegrable (fun x => (f x)⁻¹) μ a b

Tactic:
simpa only [one_div] using intervalIntegrable_one_div h hf

Result:
no goals
-- Mathlib/LinearAlgebra/FiniteDimensional/Defs.lean
theorem basisSingleton_apply (ι : Type*) [Unique ι] (h : finrank K V = 1) (v : V) (hv : v ≠ 0)
    (i : ι) : basisSingleton ι h v hv i = v

Proof state:
case refl
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
ι : Type u_1
inst✝ : Unique ι
h : finrank K V = 1
v : V
hv : v ≠ 0
⊢ (basisSingleton ι h v hv) default = v

Tactic:
simp [basisSingleton]

Result:
no goals

Proof state:
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
ι : Type u_1
inst✝ : Unique ι
h : finrank K V = 1
v : V
hv : v ≠ 0
i : ι
⊢ (basisSingleton ι h v hv) i = v

Tactic:
cases Unique.uniq ‹Unique ι› i

Result:
case refl
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
ι : Type u_1
inst✝ : Unique ι
h : finrank K V = 1
v : V
hv : v ≠ 0
⊢ (basisSingleton ι h v hv) default = v
-- Mathlib/RingTheory/Coprime/Basic.lean
theorem IsCoprime.of_mul_add_right_right (h : IsCoprime x (z * x + y)) : IsCoprime x y

Proof state:
R : Type u
inst✝ : CommSemiring R
x y z : R
h : IsCoprime x (y + z * x)
⊢ IsCoprime x y

Tactic:
exact h.of_add_mul_right_right

Result:
no goals

Proof state:
R : Type u
inst✝ : CommSemiring R
x y z : R
h : IsCoprime x (z * x + y)
⊢ IsCoprime x y

Tactic:
rw [add_comm] at h

Result:
R : Type u
inst✝ : CommSemiring R
x y z : R
h : IsCoprime x (y + z * x)
⊢ IsCoprime x y
-- Mathlib/Combinatorics/SimpleGraph/Operations.lean
/-- Adjacency in `G.replaceVertex s t` which does not involve `t` is the same as that of `G`. -/
lemma adj_replaceVertex_iff_of_ne {v w : V} (hv : v ≠ t) (hw : w ≠ t) :
    (G.replaceVertex s t).Adj v w ↔ G.Adj v w

Proof state:
V : Type u_1
G : SimpleGraph V
s t : V
inst✝ : DecidableEq V
v w : V
hv : v ≠ t
hw : w ≠ t
⊢ (G.replaceVertex s t).Adj v w ↔ G.Adj v w

Tactic:
simp [replaceVertex, hv, hw]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Meta.lean
theorem beq_iff_eq {m n : Name} : m == n ↔ m = n

Proof state:
m n : Name
⊢ (m == n) = true ↔ m = n

Tactic:
show m.beq n ↔ _

Result:
m n : Name
⊢ m.beq n = true ↔ m = n

Proof state:
m n : Name
⊢ m.beq n = true ↔ m = n

Tactic:
induction m generalizing n <;> cases n <;> simp_all [Name.beq, And.comm]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/Transvection.lean
theorem listTransvecCol_mul_last_row (i : Fin r ⊕ Unit) :
    ((listTransvecCol M).prod * M) (inr unit) i = M (inr unit) i

Proof state:
𝕜 : Type u_3
inst✝ : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
i : Fin r ⊕ Unit
⊢ ((listTransvecCol M).prod * M) (inr ()) i = M (inr ()) i

Tactic:
simpa using listTransvecCol_mul_last_row_drop M i (zero_le _)

Result:
no goals
-- Mathlib/Analysis/Normed/Algebra/TrivSqZeroExt.lean
theorem eq_smul_exp_of_invertible (x : tsze R M) [Invertible x.fst] :
    x = x.fst • exp 𝕜 (⅟ x.fst • inr x.snd)

Proof state:
𝕜 : Type u_1
R : Type u_3
M : Type u_4
inst✝¹⁸ : Field 𝕜
inst✝¹⁷ : CharZero 𝕜
inst✝¹⁶ : CommRing R
inst✝¹⁵ : AddCommGroup M
inst✝¹⁴ : Algebra 𝕜 R
inst✝¹³ : Module 𝕜 M
inst✝¹² : Module R M
inst✝¹¹ : Module Rᵐᵒᵖ M
inst✝¹⁰ : IsCentralScalar R M
inst✝⁹ : IsScalarTower 𝕜 R M
inst✝⁸ : TopologicalSpace R
inst✝⁷ : TopologicalSpace M
inst✝⁶ : IsTopologicalRing R
inst✝⁵ : IsTopologicalAddGroup M
inst✝⁴ : ContinuousSMul R M
inst✝³ : ContinuousSMul Rᵐᵒᵖ M
inst✝² : T2Space R
inst✝¹ : T2Space M
x : tsze R M
inst✝ : Invertible x.fst
⊢ x = x.fst • exp 𝕜 (⅟x.fst • inr x.snd)

Tactic:
rw [← inr_smul, exp_inr, smul_add, ← inl_one, ← inl_smul, ← inr_smul, smul_eq_mul, mul_one,
  smul_smul, mul_invOf_self, one_smul, inl_fst_add_inr_snd_eq]

Result:
no goals
-- Mathlib/LinearAlgebra/Determinant.lean
theorem det_toLin' (f : Matrix ι ι R) : LinearMap.det (Matrix.toLin' f) = Matrix.det f

Proof state:
R : Type u_1
inst✝² : CommRing R
ι : Type u_4
inst✝¹ : DecidableEq ι
inst✝ : Fintype ι
f : Matrix ι ι R
⊢ LinearMap.det (toLin' f) = f.det

Tactic:
simp only [← toLin_eq_toLin', det_toLin]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Reverse.lean
theorem reverse_neg (f : R[X]) : reverse (-f) = -reverse f

Proof state:
R : Type u_1
inst✝ : Ring R
f : R[X]
⊢ (-f).reverse = -f.reverse

Tactic:
rw [reverse, reverse, reflect_neg, natDegree_neg]

Result:
no goals
-- Mathlib/Data/List/Basic.lean
theorem foldr_concat
    (f : α → β → β) (b : β) (x : α) (xs : List α) :
    List.foldr f b (xs ++ [x]) = (List.foldr f (f x b) xs)

Proof state:
α : Type u
β : Type v
f : α → β → β
b : β
x : α
xs : List α
⊢ foldr f b (xs ++ [x]) = foldr f (f x b) xs

Tactic:
simp only [List.foldr_append, List.foldr]

Result:
no goals
-- Mathlib/Algebra/BigOperators/Group/List/Lemmas.lean
/-- A morphism into the opposite monoid acts on the product by acting on the reversed elements. -/
lemma unop_map_list_prod {F : Type*} [FunLike F M Nᵐᵒᵖ] [MonoidHomClass F M Nᵐᵒᵖ]
    (f : F) (l : List M) :
    (f l.prod).unop = (l.map (MulOpposite.unop ∘ f)).reverse.prod

Proof state:
M : Type u_4
N : Type u_5
inst✝³ : Monoid M
inst✝² : Monoid N
F : Type u_8
inst✝¹ : FunLike F M Nᵐᵒᵖ
inst✝ : MonoidHomClass F M Nᵐᵒᵖ
f : F
l : List M
⊢ MulOpposite.unop (f l.prod) = (map (MulOpposite.unop ∘ ⇑f) l).reverse.prod

Tactic:
rw [map_list_prod f l, MulOpposite.unop_list_prod, List.map_map]

Result:
no goals
-- Mathlib/ModelTheory/Equivalence.lean
lemma sup_imp {φ ψ θ : L.BoundedFormula α n} (h₁ : φ ⟹[T] θ) (h₂ : ψ ⟹[T] θ) :
    φ ⊔ ψ ⟹[T] θ := fun M v xs => by
  simp only [BoundedFormula.realize_imp, BoundedFormula.realize_sup]
  exact fun h => h.elim (h₁ M v xs) (h₂ M v xs)

Proof state:
L : Language
T : L.Theory
α : Type w
n : ℕ
φ ψ θ : L.BoundedFormula α n
h₁ : φ ⟹[T] θ
h₂ : ψ ⟹[T] θ
M : T.ModelType
v : α → ↑M
xs : Fin n → ↑M
⊢ φ.Realize v xs ∨ ψ.Realize v xs → θ.Realize v xs

Tactic:
exact fun h => h.elim (h₁ M v xs) (h₂ M v xs)

Result:
no goals

Proof state:
L : Language
T : L.Theory
α : Type w
n : ℕ
φ ψ θ : L.BoundedFormula α n
h₁ : φ ⟹[T] θ
h₂ : ψ ⟹[T] θ
M : T.ModelType
v : α → ↑M
xs : Fin n → ↑M
⊢ (φ ⊔ ψ ⟹ θ).Realize v xs

Tactic:
simp only [BoundedFormula.realize_imp, BoundedFormula.realize_sup]

Result:
L : Language
T : L.Theory
α : Type w
n : ℕ
φ ψ θ : L.BoundedFormula α n
h₁ : φ ⟹[T] θ
h₂ : ψ ⟹[T] θ
M : T.ModelType
v : α → ↑M
xs : Fin n → ↑M
⊢ φ.Realize v xs ∨ ψ.Realize v xs → θ.Realize v xs
-- Mathlib/Analysis/Analytic/Basic.lean
theorem HasFPowerSeriesOnBall.eventually_hasSum_sub (hf : HasFPowerSeriesOnBall f p x r) :
    ∀ᶠ y in 𝓝 x, HasSum (fun n : ℕ => p n fun _ : Fin n => y - x) (f y)

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
p : FormalMultilinearSeries 𝕜 E F
x : E
r : ℝ≥0∞
hf : HasFPowerSeriesOnBall f p x r
⊢ ∀ᶠ (y : E) in 𝓝 x, HasSum (fun n => (p n) fun x_1 => y - x) (f y)

Tactic:
filter_upwards [EMetric.ball_mem_nhds x hf.r_pos] with y using hf.hasSum_sub

Result:
no goals
-- Mathlib/Logic/Embedding/Set.lean
theorem Function.Embedding.sigmaSet_preimage {s : ι → Set α}
    (h : Pairwise (Disjoint on s)) (i : ι) (r : Set α) :
    Sigma.mk i ⁻¹' (Function.Embedding.sigmaSet h ⁻¹' r) = r ∩ s i

Proof state:
α : Type u_1
ι : Type u_2
s : ι → Set α
h : Pairwise (Disjoint on s)
i : ι
r : Set α
⊢ Subtype.val '' (Sigma.mk i ⁻¹' (⇑(sigmaSet h) ⁻¹' r)) = r ∩ s i

Tactic:
simp [Set.ext_iff]

Result:
no goals
-- Mathlib/Algebra/Module/Submodule/Range.lean
theorem range_codRestrict {τ₂₁ : R₂ →+* R} [RingHomSurjective τ₂₁] (p : Submodule R M)
    (f : M₂ →ₛₗ[τ₂₁] M) (hf) :
    range (codRestrict p f hf) = comap p.subtype (LinearMap.range f)

Proof state:
R : Type u_1
R₂ : Type u_2
M : Type u_5
M₂ : Type u_6
inst✝⁶ : Semiring R
inst✝⁵ : Semiring R₂
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M₂
inst✝² : Module R M
inst✝¹ : Module R₂ M₂
τ₂₁ : R₂ →+* R
inst✝ : RingHomSurjective τ₂₁
p : Submodule R M
f : M₂ →ₛₗ[τ₂₁] M
hf : ∀ (c : M₂), f c ∈ p
⊢ range (codRestrict p f hf) = comap p.subtype (range f)

Tactic:
simpa only [range_eq_map] using map_codRestrict _ _ _ _

Result:
no goals
-- Mathlib/Data/Int/CardIntervalMod.lean
theorem Ioc_filter_modEq_card (v : ℤ) :
    #{x ∈ Ioc a b | x ≡ v [ZMOD r]} = max (⌊(b - v) / (r : ℚ)⌋ - ⌊(a - v) / (r : ℚ)⌋) 0

Proof state:
a b r : ℤ
hr : 0 < r
v : ℤ
⊢ ↑(#(filter (fun x => x ≡ v [ZMOD r]) (Ioc a b))) = (⌊(↑b - ↑v) / ↑r⌋ - ⌊(↑a - ↑v) / ↑r⌋) ⊔ 0

Tactic:
simp [Ioc_filter_modEq_eq, Ioc_filter_dvd_eq, toNat_eq_max, hr]

Result:
no goals
-- Mathlib/Geometry/Manifold/MFDeriv/SpecificFunctions.lean
theorem mdifferentiableWithinAt_prod_module_iff (f : M → F₁ × F₂) :
    MDifferentiableWithinAt I 𝓘(𝕜, F₁ × F₂) f s x ↔
      MDifferentiableWithinAt I 𝓘(𝕜, F₁) (Prod.fst ∘ f) s x ∧
      MDifferentiableWithinAt I 𝓘(𝕜, F₂) (Prod.snd ∘ f) s x

Proof state:
𝕜 : Type u_1
inst✝⁹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁶ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁵ : TopologicalSpace M
inst✝⁴ : ChartedSpace H M
F₁ : Type u_17
inst✝³ : NormedAddCommGroup F₁
inst✝² : NormedSpace 𝕜 F₁
F₂ : Type u_18
inst✝¹ : NormedAddCommGroup F₂
inst✝ : NormedSpace 𝕜 F₂
s : Set M
x : M
f : M → F₁ × F₂
⊢ MDifferentiableWithinAt I (𝓘(𝕜, F₁).prod 𝓘(𝕜, F₂)) f s x ↔
    MDifferentiableWithinAt I 𝓘(𝕜, F₁) (Prod.fst ∘ f) s x ∧ MDifferentiableWithinAt I 𝓘(𝕜, F₂) (Prod.snd ∘ f) s x

Tactic:
exact mdifferentiableWithinAt_prod_iff f

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝⁹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁶ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁵ : TopologicalSpace M
inst✝⁴ : ChartedSpace H M
F₁ : Type u_17
inst✝³ : NormedAddCommGroup F₁
inst✝² : NormedSpace 𝕜 F₁
F₂ : Type u_18
inst✝¹ : NormedAddCommGroup F₂
inst✝ : NormedSpace 𝕜 F₂
s : Set M
x : M
f : M → F₁ × F₂
⊢ MDifferentiableWithinAt I 𝓘(𝕜, F₁ × F₂) f s x ↔
    MDifferentiableWithinAt I 𝓘(𝕜, F₁) (Prod.fst ∘ f) s x ∧ MDifferentiableWithinAt I 𝓘(𝕜, F₂) (Prod.snd ∘ f) s x

Tactic:
rw [modelWithCornersSelf_prod, ← chartedSpaceSelf_prod]

Result:
𝕜 : Type u_1
inst✝⁹ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝⁸ : NormedAddCommGroup E
inst✝⁷ : NormedSpace 𝕜 E
H : Type u_3
inst✝⁶ : TopologicalSpace H
I : ModelWithCorners 𝕜 E H
M : Type u_4
inst✝⁵ : TopologicalSpace M
inst✝⁴ : ChartedSpace H M
F₁ : Type u_17
inst✝³ : NormedAddCommGroup F₁
inst✝² : NormedSpace 𝕜 F₁
F₂ : Type u_18
inst✝¹ : NormedAddCommGroup F₂
inst✝ : NormedSpace 𝕜 F₂
s : Set M
x : M
f : M → F₁ × F₂
⊢ MDifferentiableWithinAt I (𝓘(𝕜, F₁).prod 𝓘(𝕜, F₂)) f s x ↔
    MDifferentiableWithinAt I 𝓘(𝕜, F₁) (Prod.fst ∘ f) s x ∧ MDifferentiableWithinAt I 𝓘(𝕜, F₂) (Prod.snd ∘ f) s x
-- Mathlib/LinearAlgebra/Matrix/ToLin.lean
theorem Matrix.range_mulVecLin (M : Matrix m n R) :
    LinearMap.range M.mulVecLin = span R (range Mᵀ)

Proof state:
R : Type u_1
inst✝¹ : CommSemiring R
m : Type u_4
n : Type u_5
inst✝ : Fintype n
M : Matrix m n R
⊢ LinearMap.range M.mulVecLin = span R (Set.range Mᵀ)

Tactic:
rw [← vecMulLinear_transpose, range_vecMulLinear]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Control/Lawful/Instances.lean
theorem map_throw [Monad m] [LawfulMonad m] {α β : Type _} (f : α → β) (e : ε) :
    f <$> (throw e : ExceptT ε m α) = (throw e : ExceptT ε m β)

Proof state:
m : Type u_1 → Type u_2
ε : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
α β : Type u_1
f : α → β
e : ε
⊢ f <$> throw e = throw e

Tactic:
simp only [ExceptT.instMonad, ExceptT.map, ExceptT.mk, throw, throwThe, MonadExceptOf.throw,
  pure_bind]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem getKeyD_ofList_of_contains_eq_false [EquivBEq α] [LawfulHashable α]
    {l : List ((a : α) × β a)} {k fallback : α}
    (contains_eq_false : (l.map Sigma.fst).contains k = false) :
    (ofList l).getKeyD k fallback = fallback

Proof state:
α : Type u
β : α → Type v
inst✝³ : BEq α
inst✝² : Hashable α
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
l : List ((a : α) × β a)
k fallback : α
contains_eq_false : (List.map Sigma.fst l).contains k = false
⊢ (ofList l).getKeyD k fallback = fallback

Tactic:
simp_to_raw using Raw₀.getKeyD_insertMany_empty_list_of_contains_eq_false

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/Nat/Gcd.lean
theorem coprime_self (n : Nat) : Coprime n n ↔ n = 1

Proof state:
n : Nat
⊢ n.Coprime n ↔ n = 1

Tactic:
simp [Coprime]

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Cofinality.lean
theorem bsup_lt_ord_of_isRegular {o : Ordinal} {f : ∀ a < o, Ordinal} {c} (hc : IsRegular c)
    (hι : o.card < c) : (∀ i hi, f i hi < c.ord) → Ordinal.bsup o f < c.ord :=
  bsup_lt_ord (by rwa [hc.cof_eq])

Proof state:
o : Ordinal.{max u_1 u_2}
f : (a : Ordinal.{max u_1 u_2}) → a < o → Ordinal.{max u_1 u_2}
c : Cardinal.{max u_1 u_2}
hc : c.IsRegular
hι : o.card < c
⊢ o.card < c.ord.cof

Tactic:
rwa [hc.cof_eq]

Result:
no goals
-- Mathlib/Analysis/Calculus/FDeriv/Add.lean
@[simp]
lemma DifferentiableAt.sub_iff_left (hg : DifferentiableAt 𝕜 g x) :
    DifferentiableAt 𝕜 (fun y => f y - g y) x ↔ DifferentiableAt 𝕜 f x

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f g : E → F
x : E
hg : DifferentiableAt 𝕜 g x
⊢ DifferentiableAt 𝕜 (fun y => f y - g y) x ↔ DifferentiableAt 𝕜 f x

Tactic:
simp only [sub_eq_add_neg, differentiableAt_neg_iff, hg, add_iff_left]

Result:
no goals
-- Mathlib/Data/ENNReal/Real.lean
@[simp]
lemma ofReal_lt_natCast {p : ℝ} {n : ℕ} (hn : n ≠ 0) : ENNReal.ofReal p < n ↔ p < n

Proof state:
p : ℝ
n : ℕ
hn : n ≠ 0
⊢ ENNReal.ofReal p < ↑n ↔ p < ↑n

Tactic:
exact mod_cast ofReal_lt_ofReal_iff (Nat.cast_pos.2 hn.bot_lt)

Result:
no goals
-- Mathlib/Topology/Instances/ENNReal/Lemmas.lean
theorem Tendsto.mul_const {f : Filter α} {m : α → ℝ≥0∞} {a b : ℝ≥0∞}
    (hm : Tendsto m f (𝓝 a)) (ha : a ≠ 0 ∨ b ≠ ∞) : Tendsto (fun x => m x * b) f (𝓝 (a * b))

Proof state:
α : Type u_1
f : Filter α
m : α → ℝ≥0∞
a b : ℝ≥0∞
hm : Tendsto m f (𝓝 a)
ha : a ≠ 0 ∨ b ≠ ⊤
⊢ Tendsto (fun x => m x * b) f (𝓝 (a * b))

Tactic:
simpa only [mul_comm] using ENNReal.Tendsto.const_mul hm ha

Result:
no goals
-- Mathlib/RingTheory/MvPolynomial/Symmetric/Defs.lean
theorem _root_.Finset.esymm_map_val {σ} (f : σ → R) (s : Finset σ) (n : ℕ) :
    (s.val.map f).esymm n = (s.powersetCard n).sum fun t => t.prod f

Proof state:
R : Type u_1
inst✝ : CommSemiring R
σ : Type u_2
f : σ → R
s : Finset σ
n : ℕ
⊢ (map f s.val).esymm n = ∑ t ∈ Finset.powersetCard n s, t.prod f

Tactic:
simp only [esymm, powersetCard_map, ← Finset.map_val_val_powersetCard, map_map]

Result:
R : Type u_1
inst✝ : CommSemiring R
σ : Type u_2
f : σ → R
s : Finset σ
n : ℕ
⊢ (map ((fun x => x.prod) ∘ (fun x => map f x) ∘ Finset.val) (Finset.powersetCard n s).val).sum =
    ∑ t ∈ Finset.powersetCard n s, t.prod f

Proof state:
R : Type u_1
inst✝ : CommSemiring R
σ : Type u_2
f : σ → R
s : Finset σ
n : ℕ
⊢ (map ((fun x => x.prod) ∘ (fun x => map f x) ∘ Finset.val) (Finset.powersetCard n s).val).sum =
    ∑ t ∈ Finset.powersetCard n s, t.prod f

Tactic:
rfl

Result:
no goals
-- Mathlib/LinearAlgebra/Contraction.lean
theorem dualTensorHom_prodMap_zero (f : Module.Dual R M) (p : P) :
    ((dualTensorHom R M P) (f ⊗ₜ[R] p)).prodMap (0 : N →ₗ[R] Q) =
      dualTensorHom R (M × N) (P × Q) ((f ∘ₗ fst R M N) ⊗ₜ inl R P Q p)

Proof state:
R : Type u
M : Type v₁
N : Type v₂
P : Type v₃
Q : Type v₄
inst✝⁸ : CommSemiring R
inst✝⁷ : AddCommMonoid M
inst✝⁶ : AddCommMonoid N
inst✝⁵ : AddCommMonoid P
inst✝⁴ : AddCommMonoid Q
inst✝³ : Module R M
inst✝² : Module R N
inst✝¹ : Module R P
inst✝ : Module R Q
f : Dual R M
p : P
⊢ ((dualTensorHom R M P) (f ⊗ₜ[R] p)).prodMap 0 =
    (dualTensorHom R (M × N) (P × Q)) ((f ∘ₗ fst R M N) ⊗ₜ[R] (inl R P Q) p)

Tactic:
ext <;>
  simp only [coe_comp, coe_inl, Function.comp_apply, prodMap_apply, dualTensorHom_apply,
    fst_apply, Prod.smul_mk, LinearMap.zero_apply, smul_zero]

Result:
no goals
-- Mathlib/Topology/VectorBundle/Basic.lean
theorem localTriv_symm_apply {b : B} (hb : b ∈ Z.baseSet i) (v : F) :
    (Z.localTriv i).symm b v = Z.coordChange i (Z.indexAt b) b v

Proof state:
R : Type u_1
B : Type u_2
F : Type u_3
inst✝³ : NontriviallyNormedField R
inst✝² : NormedAddCommGroup F
inst✝¹ : NormedSpace R F
inst✝ : TopologicalSpace B
ι : Type u_5
Z : VectorBundleCore R B F ι
i : ι
b : B
hb : b ∈ Z.baseSet i
v : F
⊢ (Z.localTriv i).symm b v = (Z.coordChange i (Z.indexAt b) b) v

Tactic:
apply (Z.localTriv i).symm_apply hb v

Result:
no goals