harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem push_inj_right {a b : α} {xs : Array α} : xs.push a = xs.push b ↔ a = b :=
  ⟨back_eq_of_push_eq, fun h => by simp [h]⟩

Proof state:
α : Type u_1
a b : α
xs : Array α
h : a = b
⊢ xs.push a = xs.push b

Tactic:
simp [h]

Result:
no goals
-- Mathlib/Analysis/Complex/UpperHalfPlane/Topology.lean
lemma comp_ofComplex_of_im_le_zero (f : ℍ → ℂ) (z z' : ℂ) (hz : z.im ≤ 0) (hz' : z'.im ≤ 0)  :
    (↑ₕ f) z = (↑ₕ f) z'

Proof state:
f : ℍ → ℂ
z z' : ℂ
hz : z.im ≤ 0
hz' : z'.im ≤ 0
⊢ (f ∘ ↑ofComplex) z = (f ∘ ↑ofComplex) z'

Tactic:
simp [ofComplex_apply_of_im_nonpos, hz, hz']

Result:
no goals
-- Mathlib/RingTheory/Polynomial/Cyclotomic/Basic.lean
theorem cyclotomic'_one (R : Type*) [CommRing R] [IsDomain R] : cyclotomic' 1 R = X - 1

Proof state:
R : Type u_2
inst✝¹ : CommRing R
inst✝ : IsDomain R
⊢ cyclotomic' 1 R = X - 1

Tactic:
simp only [cyclotomic', Finset.prod_singleton, RingHom.map_one,
  IsPrimitiveRoot.primitiveRoots_one]

Result:
no goals
-- Mathlib/Data/Int/Cast/Basic.lean
theorem cast_sub {m n} (h : m ≤ n) : ((n - m : ℕ) : R) = n - m :=
  eq_sub_of_add_eq <| by rw [← cast_add, Nat.sub_add_cancel h]

Proof state:
R : Type u
inst✝ : AddGroupWithOne R
m n : ℕ
h : m ≤ n
⊢ ↑(n - m) + ↑m = ↑n

Tactic:
rw [← cast_add, Nat.sub_add_cancel h]

Result:
no goals
-- Mathlib/Data/Set/Image.lean
theorem image_preimage_inl_union_image_preimage_inr (s : Set (α ⊕ β)) :
    Sum.inl '' (Sum.inl ⁻¹' s) ∪ Sum.inr '' (Sum.inr ⁻¹' s) = s

Proof state:
α : Type u_1
β : Type u_2
s : Set (α ⊕ β)
⊢ Sum.inl '' (Sum.inl ⁻¹' s) ∪ Sum.inr '' (Sum.inr ⁻¹' s) = s

Tactic:
rw [image_preimage_eq_inter_range, image_preimage_eq_inter_range, ← inter_union_distrib_left,
  range_inl_union_range_inr, inter_univ]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem size_insertMany_list [EquivBEq α] [LawfulHashable α] (h : m.1.WF)
    {l : List (α × β)}
    (distinct : l.Pairwise (fun a b => (a.1 == b.1) = false)) :
    (∀ (a : α), m.contains a → (l.map Prod.fst).contains a = false) →
    (insertMany m l).1.1.size = m.1.size + l.length

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
β : Type v
m : Raw₀ α fun x => β
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.val.WF
l : List (α × β)
distinct : List.Pairwise (fun a b => (a.fst == b.fst) = false) l
⊢ (∀ (a : α), m.contains a = true → (List.map Prod.fst l).contains a = false) →
    (insertMany m l).val.val.size = m.val.size + l.length

Tactic:
simp_to_model [Const.insertMany] using List.length_insertListConst

Result:
no goals
-- Mathlib/Data/Finset/Powerset.lean
theorem powersetCard_one (s : Finset α) :
    s.powersetCard 1 = s.map ⟨_, Finset.singleton_injective⟩ :=
  eq_of_veq <| Multiset.map_injective val_injective <| by simp [Multiset.powersetCard_one]

Proof state:
α : Type u_1
s : Finset α
⊢ Multiset.map val (powersetCard 1 s).val = Multiset.map val (map { toFun := singleton, inj' := ⋯ } s).val

Tactic:
simp [Multiset.powersetCard_one]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getKey!_insertListIfNewUnit_of_contains_eq_false_of_contains_eq_false [BEq α] [EquivBEq α]
    [Inhabited α] {l : List ((_ : α) × Unit)} {toInsert : List α} {k : α}
    (contains_eq_false : containsKey k l = false)
    (contains_eq_false' : toInsert.contains k = false) :
    getKey! k (insertListIfNewUnit l toInsert) = default

Proof state:
α : Type u
inst✝² : BEq α
inst✝¹ : EquivBEq α
inst✝ : Inhabited α
l : List ((_ : α) × Unit)
toInsert : List α
k : α
contains_eq_false : containsKey k l = false
contains_eq_false' : toInsert.contains k = false
⊢ getKey! k (insertListIfNewUnit l toInsert) = default

Tactic:
rw [getKey!_eq_getKey?, getKey?_insertListIfNewUnit_of_contains_eq_false_of_contains_eq_false
  contains_eq_false contains_eq_false']

Result:
α : Type u
inst✝² : BEq α
inst✝¹ : EquivBEq α
inst✝ : Inhabited α
l : List ((_ : α) × Unit)
toInsert : List α
k : α
contains_eq_false : containsKey k l = false
contains_eq_false' : toInsert.contains k = false
⊢ none.get! = default

Proof state:
α : Type u
inst✝² : BEq α
inst✝¹ : EquivBEq α
inst✝ : Inhabited α
l : List ((_ : α) × Unit)
toInsert : List α
k : α
contains_eq_false : containsKey k l = false
contains_eq_false' : toInsert.contains k = false
⊢ none.get! = default

Tactic:
simp

Result:
no goals
-- Mathlib/Order/UpperLower/Basic.lean
theorem Iic_sInf (S : Set α) : Iic (sInf S) = ⨅ a ∈ S, Iic a :=
  SetLike.ext fun c => by simp only [mem_Iic_iff, mem_iInf₂_iff, le_sInf_iff]

Proof state:
α : Type u_1
inst✝ : CompleteLattice α
S : Set α
c : α
⊢ c ∈ Iic (sInf S) ↔ c ∈ ⨅ a ∈ S, Iic a

Tactic:
simp only [mem_Iic_iff, mem_iInf₂_iff, le_sInf_iff]

Result:
no goals
-- Mathlib/Order/Disjoint.lean
theorem disjoint_left_iff (h : IsCompl y z) : Disjoint x y ↔ x ≤ z

Proof state:
α : Type u_1
inst✝¹ : DistribLattice α
inst✝ : BoundedOrder α
x y z : α
h : IsCompl y z
⊢ Disjoint x y ↔ x ≤ z

Tactic:
rw [disjoint_iff]

Result:
α : Type u_1
inst✝¹ : DistribLattice α
inst✝ : BoundedOrder α
x y z : α
h : IsCompl y z
⊢ x ⊓ y = ⊥ ↔ x ≤ z

Proof state:
α : Type u_1
inst✝¹ : DistribLattice α
inst✝ : BoundedOrder α
x y z : α
h : IsCompl y z
⊢ x ⊓ y = ⊥ ↔ x ≤ z

Tactic:
exact h.inf_left_eq_bot_iff

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/Rat/Lemmas.lean
theorem mk_eq_mkRat (num den nz c) : ⟨num, den, nz, c⟩ = mkRat num den

Proof state:
num : Int
den : Nat
nz : den ≠ 0
c : num.natAbs.Coprime den
⊢ { num := num, den := den, den_nz := nz, reduced := c } = mkRat num den

Tactic:
simp [mk_eq_normalize, normalize_eq_mkRat]

Result:
no goals
-- Mathlib/Analysis/Calculus/VectorField.lean
lemma pullback_eq_of_fderiv_eq
    {f : E → F} {M : E ≃L[𝕜] F} {x : E} (hf : M = fderiv 𝕜 f x) (V : F → F) :
    pullback 𝕜 f V x = M.symm (V (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 : E → F
M : E ≃L[𝕜] F
x : E
hf : ↑M = fderiv 𝕜 f x
V : F → F
⊢ pullback 𝕜 f V x = M.symm (V (f x))

Tactic:
simp [pullback, ← hf]

Result:
no goals
-- Mathlib/MeasureTheory/Function/LocallyIntegrable.lean
theorem continuousOn_smul [LocallyCompactSpace X] [T2Space X] {𝕜 : Type*} [NormedField 𝕜]
    [SecondCountableTopologyEither X 𝕜] [NormedSpace 𝕜 E] {f : X → E} {g : X → 𝕜} {s : Set X}
    (hs : IsLocallyClosed s) (hf : LocallyIntegrableOn f s μ) (hg : ContinuousOn g s) :
    LocallyIntegrableOn (fun x => g x • f x) s μ

Proof state:
X : Type u_1
E : Type u_3
inst✝⁸ : MeasurableSpace X
inst✝⁷ : TopologicalSpace X
inst✝⁶ : NormedAddCommGroup E
μ : Measure X
inst✝⁵ : OpensMeasurableSpace X
inst✝⁴ : LocallyCompactSpace X
inst✝³ : T2Space X
𝕜 : Type u_6
inst✝² : NormedField 𝕜
inst✝¹ : SecondCountableTopologyEither X 𝕜
inst✝ : NormedSpace 𝕜 E
f : X → E
g : X → 𝕜
s : Set X
hs : IsLocallyClosed s
hf : LocallyIntegrableOn f s μ
hg : ContinuousOn g s
⊢ LocallyIntegrableOn (fun x => g x • f x) s μ

Tactic:
rw [MeasureTheory.locallyIntegrableOn_iff hs] at hf ⊢

Result:
X : Type u_1
E : Type u_3
inst✝⁸ : MeasurableSpace X
inst✝⁷ : TopologicalSpace X
inst✝⁶ : NormedAddCommGroup E
μ : Measure X
inst✝⁵ : OpensMeasurableSpace X
inst✝⁴ : LocallyCompactSpace X
inst✝³ : T2Space X
𝕜 : Type u_6
inst✝² : NormedField 𝕜
inst✝¹ : SecondCountableTopologyEither X 𝕜
inst✝ : NormedSpace 𝕜 E
f : X → E
g : X → 𝕜
s : Set X
hs : IsLocallyClosed s
hf : ∀ k ⊆ s, IsCompact k → IntegrableOn f k μ
hg : ContinuousOn g s
⊢ ∀ k ⊆ s, IsCompact k → IntegrableOn (fun x => g x • f x) k μ

Proof state:
X : Type u_1
E : Type u_3
inst✝⁸ : MeasurableSpace X
inst✝⁷ : TopologicalSpace X
inst✝⁶ : NormedAddCommGroup E
μ : Measure X
inst✝⁵ : OpensMeasurableSpace X
inst✝⁴ : LocallyCompactSpace X
inst✝³ : T2Space X
𝕜 : Type u_6
inst✝² : NormedField 𝕜
inst✝¹ : SecondCountableTopologyEither X 𝕜
inst✝ : NormedSpace 𝕜 E
f : X → E
g : X → 𝕜
s : Set X
hs : IsLocallyClosed s
hf : ∀ k ⊆ s, IsCompact k → IntegrableOn f k μ
hg : ContinuousOn g s
⊢ ∀ k ⊆ s, IsCompact k → IntegrableOn (fun x => g x • f x) k μ

Tactic:
exact fun k hk_sub hk_c => (hf k hk_sub hk_c).continuousOn_smul (hg.mono hk_sub) hk_c

Result:
no goals
-- Mathlib/Algebra/Field/Subfield/Basic.lean
theorem coe_iSup_of_directed {ι} [hι : Nonempty ι] {S : ι → Subfield K} (hS : Directed (· ≤ ·) S) :
    ((⨆ i, S i : Subfield K) : Set K) = ⋃ i, ↑(S i) :=
  Set.ext fun x => by simp [mem_iSup_of_directed hS]

Proof state:
K : Type u
inst✝ : DivisionRing K
ι : Sort u_1
hι : Nonempty ι
S : ι → Subfield K
hS : Directed (fun x1 x2 => x1 ≤ x2) S
x : K
⊢ x ∈ ↑(⨆ i, S i) ↔ x ∈ ⋃ i, ↑(S i)

Tactic:
simp [mem_iSup_of_directed hS]

Result:
no goals
-- Mathlib/Topology/Constructions.lean
theorem map_nhds_subtype_coe_eq_nhds {x : X} (hx : p x) (h : ∀ᶠ x in 𝓝 x, p x) :
    map ((↑) : Subtype p → X) (𝓝 ⟨x, hx⟩) = 𝓝 x :=
  map_nhds_induced_of_mem <| by rw [Subtype.range_val]; exact h

Proof state:
X : Type u
inst✝ : TopologicalSpace X
p : X → Prop
x : X
hx : p x
h : ∀ᶠ (x : X) in 𝓝 x, p x
⊢ range Subtype.val ∈ 𝓝 ↑⟨x, hx⟩

Tactic:
rw [Subtype.range_val]

Result:
X : Type u
inst✝ : TopologicalSpace X
p : X → Prop
x : X
hx : p x
h : ∀ᶠ (x : X) in 𝓝 x, p x
⊢ p ∈ 𝓝 ↑⟨x, hx⟩

Proof state:
X : Type u
inst✝ : TopologicalSpace X
p : X → Prop
x : X
hx : p x
h : ∀ᶠ (x : X) in 𝓝 x, p x
⊢ p ∈ 𝓝 ↑⟨x, hx⟩

Tactic:
exact h

Result:
no goals
-- Mathlib/Analysis/RCLike/Basic.lean
theorem im_eq_conj_sub (z : K) : ↑(im z) = I * (conj z - z) / 2

Proof state:
K : Type u_1
inst✝ : RCLike K
z : K
⊢ ↑(im z) = I * ((starRingEnd K) z - z) / 2

Tactic:
rw [← neg_inj, ← ofReal_neg, ← I_mul_re, re_eq_add_conj, map_mul, conj_I, ← neg_div, ← mul_neg,
  neg_sub, mul_sub, neg_mul, sub_eq_add_neg]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Derivative.lean
theorem pow_sub_one_dvd_derivative_of_pow_dvd {p q : R[X]} {n : ℕ}
    (dvd : q ^ n ∣ p) : q ^ (n - 1) ∣ derivative p

Proof state:
case intro
R : Type u
inst✝ : CommSemiring R
q : R[X]
n : ℕ
r : R[X]
⊢ q ^ (n - 1) ∣ derivative (q ^ n * r)

Tactic:
rw [derivative_mul, derivative_pow]

Result:
case intro
R : Type u
inst✝ : CommSemiring R
q : R[X]
n : ℕ
r : R[X]
⊢ q ^ (n - 1) ∣ C ↑n * q ^ (n - 1) * derivative q * r + q ^ n * derivative r

Proof state:
R : Type u
inst✝ : CommSemiring R
p q : R[X]
n : ℕ
dvd : q ^ n ∣ p
⊢ q ^ (n - 1) ∣ derivative p

Tactic:
obtain ⟨r, rfl⟩ := dvd

Result:
case intro
R : Type u
inst✝ : CommSemiring R
q : R[X]
n : ℕ
r : R[X]
⊢ q ^ (n - 1) ∣ derivative (q ^ n * r)

Proof state:
case intro
R : Type u
inst✝ : CommSemiring R
q : R[X]
n : ℕ
r : R[X]
⊢ q ^ (n - 1) ∣ C ↑n * q ^ (n - 1) * derivative q * r + q ^ n * derivative r

Tactic:
exact (((dvd_mul_left _ _).mul_right _).mul_right _).add ((pow_dvd_pow q n.pred_le).mul_right _)

Result:
no goals
-- Mathlib/GroupTheory/Perm/Cycle/Type.lean
theorem card_fixedPoints (σ : Equiv.Perm α) :
    Fintype.card (Function.fixedPoints σ) = Fintype.card α - σ.cycleType.sum

Proof state:
case e_s
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
⊢ Finset.filter (Membership.mem (Function.fixedPoints ⇑σ)) Finset.univ = σ.supportᶜ

Tactic:
aesop

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
⊢ Fintype.card ↑(Function.fixedPoints ⇑σ) = Fintype.card α - σ.cycleType.sum

Tactic:
rw [Equiv.Perm.sum_cycleType, ← Finset.card_compl, Fintype.card_ofFinset]

Result:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
⊢ (Finset.filter (Membership.mem (Function.fixedPoints ⇑σ)) Finset.univ).card = σ.supportᶜ.card

Proof state:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
⊢ (Finset.filter (Membership.mem (Function.fixedPoints ⇑σ)) Finset.univ).card = σ.supportᶜ.card

Tactic:
congr

Result:
case e_s
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ : Perm α
⊢ Finset.filter (Membership.mem (Function.fixedPoints ⇑σ)) Finset.univ = σ.supportᶜ
-- Mathlib/Data/Nat/ModEq.lean
@[simp] lemma add_modEq_left : n + a ≡ a [MOD n]

Proof state:
n a : ℕ
⊢ n + a ≡ a [MOD n]

Tactic:
rw [ModEq, add_mod_left]

Result:
no goals
-- Mathlib/Topology/Separation/Hausdorff.lean
theorem IsCompact.isClosed [T2Space X] {s : Set X} (hs : IsCompact s) : IsClosed s :=
  isOpen_compl_iff.1 <| isOpen_iff_forall_mem_open.mpr fun x hx =>
    let ⟨u, v, _, vo, su, xv, uv⟩ :=
      SeparatedNhds.of_isCompact_isCompact hs isCompact_singleton (disjoint_singleton_right.2 hx)
    ⟨v, (uv.mono_left <| show s ≤ u from su).subset_compl_left, vo, by simpa using xv⟩

Proof state:
X : Type u_1
inst✝¹ : TopologicalSpace X
inst✝ : T2Space X
s : Set X
hs : IsCompact s
x : X
hx : x ∈ sᶜ
u v : Set X
left✝ : IsOpen u
vo : IsOpen v
su : s ⊆ u
xv : {x} ⊆ v
uv : Disjoint u v
⊢ x ∈ v

Tactic:
simpa using xv

Result:
no goals
-- Mathlib/Algebra/MvPolynomial/Division.lean
theorem monomial_one_dvd_monomial_one [Nontrivial R] {i j : σ →₀ ℕ} :
    monomial i (1 : R) ∣ monomial j 1 ↔ i ≤ j

Proof state:
σ : Type u_1
R : Type u_2
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
i j : σ →₀ ℕ
⊢ (1 = 0 ∨ i ≤ j) ∧ 1 ∣ 1 ↔ i ≤ j

Tactic:
simp_rw [one_ne_zero, false_or, dvd_rfl, and_true]

Result:
no goals

Proof state:
σ : Type u_1
R : Type u_2
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
i j : σ →₀ ℕ
⊢ (monomial i) 1 ∣ (monomial j) 1 ↔ i ≤ j

Tactic:
rw [monomial_dvd_monomial]

Result:
σ : Type u_1
R : Type u_2
inst✝¹ : CommSemiring R
inst✝ : Nontrivial R
i j : σ →₀ ℕ
⊢ (1 = 0 ∨ i ≤ j) ∧ 1 ∣ 1 ↔ i ≤ j
-- Mathlib/Algebra/Order/BigOperators/Group/Finset.lean
@[to_additive]
lemma prod_eq_one_iff_of_one_le (hf : 1 ≤ f) : ∏ i, f i = 1 ↔ f = 1 :=
  (Finset.prod_eq_one_iff_of_one_le' fun i _ ↦ hf i).trans <| by simp [funext_iff]

Proof state:
ι : Type u_1
M : Type u_4
inst✝¹ : Fintype ι
inst✝ : OrderedCommMonoid M
f : ι → M
hf : 1 ≤ f
⊢ (∀ i ∈ Finset.univ, f i = 1) ↔ f = 1

Tactic:
simp [funext_iff]

Result:
no goals
-- Mathlib/Order/Filter/Basic.lean
theorem iSup_neBot {f : ι → Filter α} : (⨆ i, f i).NeBot ↔ ∃ i, (f i).NeBot

Proof state:
α : Type u
ι : Sort x
f : ι → Filter α
⊢ (⨆ i, f i).NeBot ↔ ∃ i, (f i).NeBot

Tactic:
simp [neBot_iff]

Result:
no goals
-- Mathlib/NumberTheory/NumberField/CanonicalEmbedding/Basic.lean
theorem negAt_signSet_apply_isReal (x : mixedSpace K) (w : {w // IsReal w}) :
    (negAt (signSet x) x).1 w = |x.1 w|

Proof state:
K : Type u_1
inst✝ : Field K
x : mixedSpace K
w : { w // w.IsReal }
⊢ ((negAt (signSet x)) x).1 w = |x.1 w|

Tactic:
by_cases hw : x.1 w ≤ 0

Result:
case pos
K : Type u_1
inst✝ : Field K
x : mixedSpace K
w : { w // w.IsReal }
hw : x.1 w ≤ 0
⊢ ((negAt (signSet x)) x).1 w = |x.1 w|

case neg
K : Type u_1
inst✝ : Field K
x : mixedSpace K
w : { w // w.IsReal }
hw : ¬x.1 w ≤ 0
⊢ ((negAt (signSet x)) x).1 w = |x.1 w|

Proof state:
case pos
K : Type u_1
inst✝ : Field K
x : mixedSpace K
w : { w // w.IsReal }
hw : x.1 w ≤ 0
⊢ ((negAt (signSet x)) x).1 w = |x.1 w|

Tactic:
rw [negAt_apply_isReal_and_mem _ hw, abs_of_nonpos hw]

Result:
no goals

Proof state:
case neg
K : Type u_1
inst✝ : Field K
x : mixedSpace K
w : { w // w.IsReal }
hw : ¬x.1 w ≤ 0
⊢ ((negAt (signSet x)) x).1 w = |x.1 w|

Tactic:
rw [negAt_apply_isReal_and_not_mem _ hw, abs_of_pos (lt_of_not_ge hw)]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/Raw.lean
theorem Const.getThenInsertIfNew?_fst_val [BEq α] [Hashable α] {m : Raw₀ α (fun _ => β)} {a : α}
    {b : β} : (Raw.Const.getThenInsertIfNew? m.val a b).1 =
      (Raw₀.Const.getThenInsertIfNew? m a b).1

Proof state:
α : Type u
β : Type v
inst✝¹ : BEq α
inst✝ : Hashable α
m : Raw₀ α fun x => β
a : α
b : β
⊢ (Raw.Const.getThenInsertIfNew? m.val a b).fst = (Raw₀.Const.getThenInsertIfNew? m a b).fst

Tactic:
simp [Raw.Const.getThenInsertIfNew?, m.2]

Result:
no goals
-- Mathlib/Geometry/Manifold/ContMDiff/Constructions.lean
theorem ContMDiffWithinAt.prod_mk_space {f : M → E'} {g : M → F'}
    (hf : ContMDiffWithinAt I 𝓘(𝕜, E') n f s x) (hg : ContMDiffWithinAt I 𝓘(𝕜, F') n g s x) :
    ContMDiffWithinAt I 𝓘(𝕜, E' × F') n (fun x => (f x, g x)) 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
E' : Type u_5
inst✝³ : NormedAddCommGroup E'
inst✝² : NormedSpace 𝕜 E'
F' : Type u_11
inst✝¹ : NormedAddCommGroup F'
inst✝ : NormedSpace 𝕜 F'
s : Set M
x : M
n : WithTop ℕ∞
f : M → E'
g : M → F'
hf : ContMDiffWithinAt I 𝓘(𝕜, E') n f s x
hg : ContMDiffWithinAt I 𝓘(𝕜, F') n g s x
⊢ ContMDiffWithinAt I 𝓘(𝕜, E' × F') n (fun x => (f x, g x)) s x

Tactic:
rw [contMDiffWithinAt_iff] at *

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
E' : Type u_5
inst✝³ : NormedAddCommGroup E'
inst✝² : NormedSpace 𝕜 E'
F' : Type u_11
inst✝¹ : NormedAddCommGroup F'
inst✝ : NormedSpace 𝕜 F'
s : Set M
x : M
n : WithTop ℕ∞
f : M → E'
g : M → F'
hf :
  ContinuousWithinAt f s x ∧
    ContDiffWithinAt 𝕜 n (↑(extChartAt 𝓘(𝕜, E') (f x)) ∘ f ∘ ↑(extChartAt I x).symm)
      (↑(extChartAt I x).symm ⁻¹' s ∩ range ↑I) (↑(extChartAt I x) x)
hg :
  ContinuousWithinAt g s x ∧
    ContDiffWithinAt 𝕜 n (↑(extChartAt 𝓘(𝕜, F') (g x)) ∘ g ∘ ↑(extChartAt I x).symm)
      (↑(extChartAt I x).symm ⁻¹' s ∩ range ↑I) (↑(extChartAt I x) x)
⊢ ContinuousWithinAt (fun x => (f x, g x)) s x ∧
    ContDiffWithinAt 𝕜 n (↑(extChartAt 𝓘(𝕜, E' × F') (f x, g x)) ∘ (fun x => (f x, g x)) ∘ ↑(extChartAt I x).symm)
      (↑(extChartAt I x).symm ⁻¹' s ∩ range ↑I) (↑(extChartAt I x) 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
E' : Type u_5
inst✝³ : NormedAddCommGroup E'
inst✝² : NormedSpace 𝕜 E'
F' : Type u_11
inst✝¹ : NormedAddCommGroup F'
inst✝ : NormedSpace 𝕜 F'
s : Set M
x : M
n : WithTop ℕ∞
f : M → E'
g : M → F'
hf :
  ContinuousWithinAt f s x ∧
    ContDiffWithinAt 𝕜 n (↑(extChartAt 𝓘(𝕜, E') (f x)) ∘ f ∘ ↑(extChartAt I x).symm)
      (↑(extChartAt I x).symm ⁻¹' s ∩ range ↑I) (↑(extChartAt I x) x)
hg :
  ContinuousWithinAt g s x ∧
    ContDiffWithinAt 𝕜 n (↑(extChartAt 𝓘(𝕜, F') (g x)) ∘ g ∘ ↑(extChartAt I x).symm)
      (↑(extChartAt I x).symm ⁻¹' s ∩ range ↑I) (↑(extChartAt I x) x)
⊢ ContinuousWithinAt (fun x => (f x, g x)) s x ∧
    ContDiffWithinAt 𝕜 n (↑(extChartAt 𝓘(𝕜, E' × F') (f x, g x)) ∘ (fun x => (f x, g x)) ∘ ↑(extChartAt I x).symm)
      (↑(extChartAt I x).symm ⁻¹' s ∩ range ↑I) (↑(extChartAt I x) x)

Tactic:
exact ⟨hf.1.prod hg.1, hf.2.prod hg.2⟩

Result:
no goals
-- Mathlib/Data/Complex/Trigonometric.lean
theorem ofReal_sinh_ofReal_re (x : ℝ) : ((sinh x).re : ℂ) = sinh x :=
  conj_eq_iff_re.1 <| by rw [← sinh_conj, conj_ofReal]

Proof state:
x : ℝ
⊢ (starRingEnd ℂ) (sinh ↑x) = sinh ↑x

Tactic:
rw [← sinh_conj, conj_ofReal]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Bool.lean
theorem iff_or_self : ∀ {a b : Bool}, (b = (a || b)) ↔ (a → b)

Proof state:
⊢ ∀ {a b : Bool}, b = (a || b) ↔ a = true → b = true

Tactic:
decide

Result:
no goals
-- Mathlib/Data/Finsupp/NeLocus.lean
theorem neLocus_sub_right : neLocus (f₁ - g) (f₂ - g) = neLocus f₁ f₂

Proof state:
α : Type u_1
N : Type u_3
inst✝² : DecidableEq α
inst✝¹ : DecidableEq N
inst✝ : AddGroup N
f₁ f₂ g : α →₀ N
⊢ (f₁ - g).neLocus (f₂ - g) = f₁.neLocus f₂

Tactic:
simpa only [sub_eq_add_neg] using neLocus_add_right _ _ _

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/Orientation.lean
theorem finOrthonormalBasis_orientation (hn : 0 < n) (h : finrank ℝ E = n)
    (x : Orientation ℝ E (Fin n)) : (x.finOrthonormalBasis hn h).toBasis.orientation = x

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
n : ℕ
hn : 0 < n
h : finrank ℝ E = n
x : Orientation ℝ E (Fin n)
this✝ : Nonempty (Fin n)
this : FiniteDimensional ℝ E
⊢ (Orientation.finOrthonormalBasis hn h x).toBasis.orientation = x

Tactic:
exact ((@stdOrthonormalBasis _ _ _ _ _ this).reindex <|
  finCongr h).orientation_adjustToOrientation x

Result:
no goals

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
n : ℕ
hn : 0 < n
h : finrank ℝ E = n
x : Orientation ℝ E (Fin n)
this : Nonempty (Fin n)
⊢ (Orientation.finOrthonormalBasis hn h x).toBasis.orientation = x

Tactic:
haveI : FiniteDimensional ℝ E := .of_finrank_pos <| h.symm ▸ hn

Result:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
n : ℕ
hn : 0 < n
h : finrank ℝ E = n
x : Orientation ℝ E (Fin n)
this✝ : Nonempty (Fin n)
this : FiniteDimensional ℝ E
⊢ (Orientation.finOrthonormalBasis hn h x).toBasis.orientation = x

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
n : ℕ
hn : 0 < n
h : finrank ℝ E = n
x : Orientation ℝ E (Fin n)
⊢ (Orientation.finOrthonormalBasis hn h x).toBasis.orientation = x

Tactic:
haveI := Fin.pos_iff_nonempty.1 hn

Result:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace ℝ E
n : ℕ
hn : 0 < n
h : finrank ℝ E = n
x : Orientation ℝ E (Fin n)
this : Nonempty (Fin n)
⊢ (Orientation.finOrthonormalBasis hn h x).toBasis.orientation = x
-- Mathlib/Analysis/SpecialFunctions/ContinuousFunctionalCalculus/PosPart.lean
lemma CStarAlgebra.linear_combination_nonneg (x : A) :
    ((ℜ x : A)⁺ - (ℜ x : A)⁻) + (I • (ℑ x : A)⁺ - I • (ℑ x : A)⁻) = x

Proof state:
A : Type u_1
inst✝⁹ : NonUnitalRing A
inst✝⁸ : Module ℂ A
inst✝⁷ : SMulCommClass ℂ A A
inst✝⁶ : IsScalarTower ℂ A A
inst✝⁵ : StarRing A
inst✝⁴ : TopologicalSpace A
inst✝³ : StarModule ℂ A
inst✝² : NonUnitalContinuousFunctionalCalculus ℝ IsSelfAdjoint
inst✝¹ : PartialOrder A
inst✝ : StarOrderedRing A
x : A
⊢ (↑(ℜ x))⁺ - (↑(ℜ x))⁻ + (I • (↑(ℑ x))⁺ - I • (↑(ℑ x))⁻) = x

Tactic:
rw [CFC.posPart_sub_negPart _ (ℜ x).2, ← smul_sub, CFC.posPart_sub_negPart _ (ℑ x).2,
  realPart_add_I_smul_imaginaryPart x]

Result:
no goals
-- Mathlib/Data/Num/Lemmas.lean
theorem cmp_swap (m n) : (cmp m n).swap = cmp n m

Proof state:
m n : Num
⊢ (m.cmp n).swap = n.cmp m

Tactic:
cases m <;> cases n <;> try { rfl }

Result:
case pos.pos
a✝¹ a✝ : PosNum
⊢ ((pos a✝¹).cmp (pos a✝)).swap = (pos a✝).cmp (pos a✝¹)

Proof state:
case pos.pos
a✝¹ a✝ : PosNum
⊢ ((pos a✝¹).cmp (pos a✝)).swap = (pos a✝).cmp (pos a✝¹)

Tactic:
apply PosNum.cmp_swap

Result:
no goals

Proof state:
case pos.zero
a✝ : PosNum
⊢ ((pos a✝).cmp zero).swap = zero.cmp (pos a✝)

Tactic:
rfl

Result:
no goals
-- Mathlib/Algebra/Order/Monoid/Unbundled/WithTop.lean
@[simp] lemma add_top (x : WithTop α) : x + ⊤ = ⊤

Proof state:
α : Type u
inst✝ : Add α
x : WithTop α
⊢ x + ⊤ = ⊤

Tactic:
cases x <;> rfl

Result:
no goals
-- Mathlib/Algebra/Order/Floor.lean
theorem map_fract (f : F) (hf : StrictMono f) (a : α) : fract (f a) = f (fract a)

Proof state:
F : Type u_1
α : Type u_2
β : Type u_3
inst✝⁵ : LinearOrderedRing α
inst✝⁴ : LinearOrderedRing β
inst✝³ : FloorRing α
inst✝² : FloorRing β
inst✝¹ : FunLike F α β
inst✝ : RingHomClass F α β
f : F
hf : StrictMono ⇑f
a : α
⊢ fract (f a) = f (fract a)

Tactic:
simp_rw [fract, map_sub, map_intCast, map_floor _ hf]

Result:
no goals