harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/RingTheory/WittVector/FrobeniusFractionField.lean
theorem root_exists (n : ℕ) (a₁ a₂ : 𝕎 k) (bs : Fin (n + 1) → k) (ha₁ : a₁.coeff 0 ≠ 0)
    (ha₂ : a₂.coeff 0 ≠ 0) : ∃ b : k, (succNthDefiningPoly p n a₁ a₂ bs).IsRoot b :=
  IsAlgClosed.exists_root _ <| by
    simp only [succNthDefiningPoly_degree p n a₁ a₂ bs ha₁ ha₂, ne_eq, Nat.cast_eq_zero,
      hp.out.ne_zero, not_false_eq_true]

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
k : Type u_1
inst✝² : Field k
inst✝¹ : CharP k p
inst✝ : IsAlgClosed k
n : ℕ
a₁ a₂ : 𝕎 k
bs : Fin (n + 1) → k
ha₁ : a₁.coeff 0 ≠ 0
ha₂ : a₂.coeff 0 ≠ 0
⊢ (succNthDefiningPoly p n a₁ a₂ bs).degree ≠ 0

Tactic:
simp only [succNthDefiningPoly_degree p n a₁ a₂ bs ha₁ ha₂, ne_eq, Nat.cast_eq_zero,
  hp.out.ne_zero, not_false_eq_true]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Girth.lean
@[simp]
lemma egirth_eq_top : G.egirth = ⊤ ↔ G.IsAcyclic

Proof state:
α : Type u_1
G : SimpleGraph α
⊢ G.egirth = ⊤ ↔ G.IsAcyclic

Tactic:
simp [egirth, IsAcyclic]

Result:
no goals
-- Mathlib/Analysis/RCLike/Basic.lean
theorem conj_smul (r : ℝ) (z : K) : conj (r • z) = r • conj z

Proof state:
K : Type u_1
inst✝ : RCLike K
r : ℝ
z : K
⊢ (starRingEnd K) (r • z) = r • (starRingEnd K) z

Tactic:
rw [conj_eq_re_sub_im, conj_eq_re_sub_im, smul_re, smul_im, ofReal_mul, ofReal_mul,
  real_smul_eq_coe_mul r (_ - _), mul_sub, mul_assoc]

Result:
no goals
-- Mathlib/Data/Fin/Basic.lean
theorem pred_last (h := Fin.ext_iff.not.2 last_pos'.ne') :
    pred (last (n + 1)) h = last n

Proof state:
n : ℕ
h : optParam (¬last (n + 1) = 0) ⋯
⊢ (last (n + 1)).pred h = last n

Tactic:
simp_rw [← succ_last, pred_succ]

Result:
no goals
-- Mathlib/Data/Real/EReal.lean
lemma strictAnti_div_right_of_neg (h : b < 0) (h' : b ≠ ⊥) : StrictAnti fun a ↦ a / b

Proof state:
b : EReal
h : b < 0
h' : b ≠ ⊥
a a' : EReal
a_lt_a' : a < a'
hyp : a' / b = a / b
⊢ a = a'

Tactic:
rw [← @EReal.mul_div_cancel a b h' (ne_top_of_lt h) (ne_of_lt h), ← hyp,
  @EReal.mul_div_cancel a' b h' (ne_top_of_lt h) (ne_of_lt h)]

Result:
no goals

Proof state:
b : EReal
h : b < 0
h' : b ≠ ⊥
a a' : EReal
a_lt_a' : a < a'
⊢ a' / b ≠ a / b

Tactic:
intro hyp

Result:
b : EReal
h : b < 0
h' : b ≠ ⊥
a a' : EReal
a_lt_a' : a < a'
hyp : a' / b = a / b
⊢ False

Proof state:
b : EReal
h : b < 0
h' : b ≠ ⊥
⊢ StrictAnti fun a => a / b

Tactic:
intro a a' a_lt_a'

Result:
b : EReal
h : b < 0
h' : b ≠ ⊥
a a' : EReal
a_lt_a' : a < a'
⊢ (fun a => a / b) a' < (fun a => a / b) a

Proof state:
b : EReal
h : b < 0
h' : b ≠ ⊥
a a' : EReal
a_lt_a' : a < a'
⊢ (fun a => a / b) a' < (fun a => a / b) a

Tactic:
simp only

Result:
b : EReal
h : b < 0
h' : b ≠ ⊥
a a' : EReal
a_lt_a' : a < a'
⊢ a' / b < a / b

Proof state:
b : EReal
h : b < 0
h' : b ≠ ⊥
a a' : EReal
a_lt_a' : a < a'
hyp : a' / b = a / b
⊢ False

Tactic:
apply ne_of_lt a_lt_a'

Result:
b : EReal
h : b < 0
h' : b ≠ ⊥
a a' : EReal
a_lt_a' : a < a'
hyp : a' / b = a / b
⊢ a = a'

Proof state:
b : EReal
h : b < 0
h' : b ≠ ⊥
a a' : EReal
a_lt_a' : a < a'
⊢ a' / b < a / b

Tactic:
apply lt_of_le_of_ne <| div_le_div_right_of_nonpos (le_of_lt h) (le_of_lt a_lt_a')

Result:
b : EReal
h : b < 0
h' : b ≠ ⊥
a a' : EReal
a_lt_a' : a < a'
⊢ a' / b ≠ a / b
-- Mathlib/Algebra/BigOperators/Fin.lean
theorem prod_const [CommMonoid α] (n : ℕ) (x : α) : ∏ _i : Fin n, x = x ^ n

Proof state:
α : Type u_1
inst✝ : CommMonoid α
n : ℕ
x : α
⊢ ∏ _i : Fin n, x = x ^ n

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem extract_loop_of_ge (as bs : Array α) (size start : Nat) (h : start ≥ as.size) :
    extract.loop as size start bs = bs

Proof state:
α : Type u_1
as bs : Array α
size start : Nat
h : start ≥ as.size
⊢ extract.loop as size start bs = bs

Tactic:
rw [extract.loop, dif_neg (Nat.not_lt_of_ge h)]

Result:
no goals
-- Mathlib/MeasureTheory/Constructions/BorelSpace/Order.lean
theorem borel_eq_generateFrom_Ioc (α : Type*) [TopologicalSpace α] [SecondCountableTopology α]
    [LinearOrder α] [OrderTopology α] :
    borel α = .generateFrom { S : Set α | ∃ l u, l < u ∧ Ioc l u = S }

Proof state:
α : Type u_5
inst✝³ : TopologicalSpace α
inst✝² : SecondCountableTopology α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
⊢ borel α = MeasurableSpace.generateFrom {S | ∃ l u, l < u ∧ Ioc l u = S}

Tactic:
simpa only [exists_prop, mem_univ, true_and] using
  (@dense_univ α _).borel_eq_generateFrom_Ioc_mem_aux (fun _ _ => mem_univ _) fun _ _ _ _ =>
    mem_univ _

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Erase.lean
theorem eraseIdx_cast {l : Vector α n} {k : Nat} (h : k < m) :
    eraseIdx (l.cast w) k h = (eraseIdx l k).cast (by omega)

Proof state:
case mk
α : Type u_1
m k : Nat
h : k < m
l : Array α
w : l.size = m
⊢ (Vector.cast w { toArray := l, size_toArray := ⋯ }).eraseIdx k h =
    Vector.cast ⋯ ({ toArray := l, size_toArray := ⋯ }.eraseIdx k ⋯)

Tactic:
simp

Result:
no goals

Proof state:
α : Type ?u.35621
n m : Nat
w : n = m
l : Vector α n
k : Nat
h : k < m
⊢ n - 1 = m - 1

Tactic:
omega

Result:
no goals

Proof state:
α : Type u_1
n m : Nat
w : n = m
l : Vector α n
k : Nat
h : k < m
⊢ (Vector.cast w l).eraseIdx k h = Vector.cast ⋯ (l.eraseIdx k ⋯)

Tactic:
rcases l with ⟨l, rfl⟩

Result:
case mk
α : Type u_1
m k : Nat
h : k < m
l : Array α
w : l.size = m
⊢ (Vector.cast w { toArray := l, size_toArray := ⋯ }).eraseIdx k h =
    Vector.cast ⋯ ({ toArray := l, size_toArray := ⋯ }.eraseIdx k ⋯)
-- Mathlib/GroupTheory/Perm/Cycle/Type.lean
theorem isConj_iff_cycleType_eq {σ τ : Perm α} : IsConj σ τ ↔ σ.cycleType = τ.cycleType :=
  ⟨fun h => by
    obtain ⟨π, rfl⟩ := isConj_iff.1 h
    rw [cycleType_conj], isConj_of_cycleType_eq⟩

Proof state:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ τ : Perm α
h : IsConj σ τ
⊢ σ.cycleType = τ.cycleType

Tactic:
obtain ⟨π, rfl⟩ := isConj_iff.1 h

Result:
case intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ π : Perm α
h : IsConj σ (π * σ * π⁻¹)
⊢ σ.cycleType = (π * σ * π⁻¹).cycleType

Proof state:
case intro
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
σ π : Perm α
h : IsConj σ (π * σ * π⁻¹)
⊢ σ.cycleType = (π * σ * π⁻¹).cycleType

Tactic:
rw [cycleType_conj]

Result:
no goals
-- Mathlib/CategoryTheory/Enriched/Ordinary/Basic.lean
@[simp]
lemma eHomWhiskerRight_id (X Y : C) : eHomWhiskerRight V (𝟙 X) Y = 𝟙 _

Proof state:
V : Type u'
inst✝³ : Category.{v', u'} V
inst✝² : MonoidalCategory V
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : EnrichedOrdinaryCategory V C
X Y : C
⊢ eHomWhiskerRight V (𝟙 X) Y = 𝟙 (EnrichedCategory.Hom X Y)

Tactic:
simp [eHomWhiskerRight]

Result:
no goals
-- Mathlib/Data/Set/Basic.lean
theorem union_empty_iff {s t : Set α} : s ∪ t = ∅ ↔ s = ∅ ∧ t = ∅

Proof state:
α : Type u
s t : Set α
⊢ s ∪ t ⊆ ∅ ↔ s ⊆ ∅ ∧ t ⊆ ∅

Tactic:
exact union_subset_iff

Result:
no goals

Proof state:
α : Type u
s t : Set α
⊢ s ∪ t = ∅ ↔ s = ∅ ∧ t = ∅

Tactic:
simp only [← subset_empty_iff]

Result:
α : Type u
s t : Set α
⊢ s ∪ t ⊆ ∅ ↔ s ⊆ ∅ ∧ t ⊆ ∅
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem append_empty (as : Vector α n) : as ++ (#v[] : Vector α 0) = as

Proof state:
α : Type u_1
n : Nat
as : Vector α n
⊢ as ++ { toArray := #[], size_toArray := ⋯ } = as

Tactic:
rw [← toArray_inj, toArray_append, Array.append_empty]

Result:
no goals
-- Mathlib/Algebra/Group/Action/Defs.lean
@[to_additive]
lemma SMulCommClass.of_mul_smul_one {M N} [Monoid N] [SMul M N]
    (H : ∀ (x : M) (y : N), y * x • (1 : N) = x • y) : SMulCommClass M N N :=
  ⟨fun x y z ↦ by rw [← H x z, smul_eq_mul, ← H, smul_eq_mul, mul_assoc]⟩

Proof state:
M : Type u_9
N : Type u_10
inst✝¹ : Monoid N
inst✝ : SMul M N
H : ∀ (x : M) (y : N), y * x • 1 = x • y
x : M
y z : N
⊢ x • y • z = y • x • z

Tactic:
rw [← H x z, smul_eq_mul, ← H, smul_eq_mul, mul_assoc]

Result:
no goals
-- Mathlib/Analysis/RCLike/Basic.lean
lemma neg_iff_exists_ofReal : z < 0 ↔ ∃ x < (0 : ℝ), x = z

Proof state:
K : Type u_1
inst✝ : RCLike K
z : K
⊢ z < 0 ↔ ∃ x < 0, ↑x = z

Tactic:
simp_rw [neg_iff (K := K), ext_iff (K := K)]

Result:
K : Type u_1
inst✝ : RCLike K
z : K
⊢ re z < 0 ∧ im z = 0 ↔ ∃ x < 0, re ↑x = re z ∧ im ↑x = im z

Proof state:
K : Type u_1
inst✝ : RCLike K
z : K
⊢ re z < 0 ∧ im z = 0 ↔ ∃ x < 0, re ↑x = re z ∧ im ↑x = im z

Tactic:
aesop

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

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

Tactic:
rw [Coprime, Coprime, gcd_add_mul_right_left]

Result:
no goals
-- Mathlib/Data/Matroid/Basic.lean
theorem IsBasis.isBasis_union (hIX : M.IsBasis I X) (hIY : M.IsBasis I Y) :
    M.IsBasis I (X ∪ Y)

Proof state:
α : Type u_1
M : Matroid α
I X Y : Set α
hIX : M.IsBasis I X
hIY : M.IsBasis I Y
⊢ M.IsBasis I (X ∪ Y)

Tactic:
convert hIX.union_isBasis_union hIY _ <;> rw [union_self]

Result:
α : Type u_1
M : Matroid α
I X Y : Set α
hIX : M.IsBasis I X
hIY : M.IsBasis I Y
⊢ M.Indep I

Proof state:
α : Type u_1
M : Matroid α
I X Y : Set α
hIX : M.IsBasis I X
hIY : M.IsBasis I Y
⊢ M.Indep I

Tactic:
exact hIX.indep

Result:
no goals
-- Mathlib/Order/SymmDiff.lean
theorem inf_symmDiff_symmDiff : (a ⊓ b) ∆ (a ∆ b) = a ⊔ b

Proof state:
α : Type u_2
inst✝ : GeneralizedCoheytingAlgebra α
a b : α
⊢ (a ⊓ b) ∆ (a ∆ b) = a ⊔ b

Tactic:
rw [symmDiff_comm, symmDiff_symmDiff_inf]

Result:
no goals
-- Mathlib/Algebra/Order/Group/Pointwise/Interval.lean
theorem image_mul_right_Ioc (a b : α) {c : α} (h : 0 < c) :
    (fun x => x * c) '' Ioc a b = Ioc (a * c) (b * c) :=
  ((Units.mk0 c h.ne').mulRight.image_eq_preimage _).trans (by simp [h, division_def])

Proof state:
α : Type u_1
inst✝ : LinearOrderedField α
a b c : α
h : 0 < c
⊢ ⇑(Equiv.symm (Units.mk0 c ⋯).mulRight) ⁻¹' Ioc a b = Ioc (a * c) (b * c)

Tactic:
simp [h, division_def]

Result:
no goals
-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Isometric.lean
lemma norm_cfcₙHom (a : A) (f : C(σₙ 𝕜 a, 𝕜)₀) (ha : p a

Proof state:
𝕜 : Type u_1
A : Type u_2
p : outParam (A → Prop)
inst✝⁶ : RCLike 𝕜
inst✝⁵ : NonUnitalNormedRing A
inst✝⁴ : StarRing A
inst✝³ : NormedSpace 𝕜 A
inst✝² : IsScalarTower 𝕜 A A
inst✝¹ : SMulCommClass 𝕜 A A
inst✝ : NonUnitalIsometricContinuousFunctionalCalculus 𝕜 A p
a : A
f : C(↑(σₙ 𝕜 a), 𝕜)₀
ha : autoParam (p a) _auto✝
⊢ ‖(cfcₙHom ⋯) f‖ = ‖f‖

Tactic:
refine isometry_cfcₙHom a |>.norm_map_of_map_zero (map_zero _) f

Result:
no goals
-- Mathlib/RingTheory/HahnSeries/Basic.lean
@[simp]
lemma mk_eq_zero (f : Γ → R) (h) : HahnSeries.mk f h = 0 ↔ f = 0

Proof state:
Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : Zero R
f : Γ → R
h : (Function.support f).IsPWO
⊢ { coeff := f, isPWO_support' := h } = 0 ↔ f = 0

Tactic:
rw [HahnSeries.ext_iff]

Result:
Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : Zero R
f : Γ → R
h : (Function.support f).IsPWO
⊢ { coeff := f, isPWO_support' := h }.coeff = coeff 0 ↔ f = 0

Proof state:
Γ : Type u_1
R : Type u_3
inst✝¹ : PartialOrder Γ
inst✝ : Zero R
f : Γ → R
h : (Function.support f).IsPWO
⊢ { coeff := f, isPWO_support' := h }.coeff = coeff 0 ↔ f = 0

Tactic:
rfl

Result:
no goals
-- Mathlib/Topology/MetricSpace/HausdorffDimension.lean
theorem hausdorffMeasure_of_dimH_lt {s : Set X} {d : ℝ≥0} (h : dimH s < d) : μH[d] s = 0

Proof state:
case intro.intro
X : Type u_2
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
s : Set X
d : ℝ≥0
h : ⨆ d, ⨆ (_ : μH[↑d] s = ⊤), ↑d < ↑d
d' : ℝ≥0
hsd' : ⨆ d, ⨆ (_ : μH[↑d] s = ⊤), ↑d < ↑d'
hd'd : ↑d' < ↑d
⊢ μH[↑d] s = 0

Tactic:
exact (hausdorffMeasure_zero_or_top hd'd s).resolve_right fun h₂ => hsd'.not_le <|
  le_iSup₂ (α := ℝ≥0∞) d' h₂

Result:
no goals

Proof state:
X : Type u_2
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
s : Set X
d : ℝ≥0
h : dimH s < ↑d
⊢ μH[↑d] s = 0

Tactic:
rw [dimH_def] at h

Result:
X : Type u_2
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
s : Set X
d : ℝ≥0
h : ⨆ d, ⨆ (_ : μH[↑d] s = ⊤), ↑d < ↑d
⊢ μH[↑d] s = 0

Proof state:
X : Type u_2
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
s : Set X
d : ℝ≥0
h : ⨆ d, ⨆ (_ : μH[↑d] s = ⊤), ↑d < ↑d
⊢ μH[↑d] s = 0

Tactic:
rcases ENNReal.lt_iff_exists_nnreal_btwn.1 h with ⟨d', hsd', hd'd⟩

Result:
case intro.intro
X : Type u_2
inst✝² : EMetricSpace X
inst✝¹ : MeasurableSpace X
inst✝ : BorelSpace X
s : Set X
d : ℝ≥0
h : ⨆ d, ⨆ (_ : μH[↑d] s = ⊤), ↑d < ↑d
d' : ℝ≥0
hsd' : ⨆ d, ⨆ (_ : μH[↑d] s = ⊤), ↑d < ↑d'
hd'd : ↑d' < ↑d
⊢ μH[↑d] s = 0
-- Mathlib/SetTheory/Game/Birthday.lean
theorem le_birthday (x : Game) : x ≤ x.birthday.toGame

Proof state:
x : Game
y : PGame
hy₁ : ⟦y⟧ = x
hy₂ : y.birthday = x.birthday
⊢ y.birthday.toPGame ≤ (birthday ⟦y⟧).toPGame

Tactic:
rw [toPGame_le_iff, hy₁, hy₂]

Result:
no goals

Proof state:
x : Game
y : PGame
hy₁ : ⟦y⟧ = x
hy₂ : y.birthday = x.birthday
⊢ x ≤ toGame x.birthday

Tactic:
rw [← hy₁]

Result:
x : Game
y : PGame
hy₁ : ⟦y⟧ = x
hy₂ : y.birthday = x.birthday
⊢ ⟦y⟧ ≤ toGame (birthday ⟦y⟧)

Proof state:
x : Game
⊢ x ≤ toGame x.birthday

Tactic:
let ⟨y, hy₁, hy₂⟩ := birthday_eq_pGameBirthday x

Result:
x : Game
y : PGame
hy₁ : ⟦y⟧ = x
hy₂ : y.birthday = x.birthday
⊢ x ≤ toGame x.birthday

Proof state:
x : Game
y : PGame
hy₁ : ⟦y⟧ = x
hy₂ : y.birthday = x.birthday
⊢ ⟦y⟧ ≤ toGame (birthday ⟦y⟧)

Tactic:
apply (y.le_birthday).trans

Result:
x : Game
y : PGame
hy₁ : ⟦y⟧ = x
hy₂ : y.birthday = x.birthday
⊢ y.birthday.toPGame ≤ (birthday ⟦y⟧).toPGame
-- Mathlib/NumberTheory/ModularForms/JacobiTheta/TwoVariable.lean
lemma hasFDerivAt_jacobiTheta₂_term (n : ℤ) (z τ : ℂ) :
    HasFDerivAt (fun p : ℂ × ℂ ↦ jacobiTheta₂_term n p.1 p.2)
    (jacobiTheta₂_term_fderiv n z τ) (z, τ)

Proof state:
n : ℤ
z τ : ℂ
f : ℂ × ℂ → ℂ := fun p => 2 * ↑π * I * ↑n * p.1 + ↑π * I * ↑n ^ 2 * p.2
⊢ HasFDerivAt (fun p => jacobiTheta₂_term n p.1 p.2) (jacobiTheta₂_term_fderiv n z τ) (z, τ)

Tactic:
suffices HasFDerivAt f ((2 * π * I * n) • (ContinuousLinearMap.fst ℂ ℂ ℂ)
  + (π * I * n ^ 2) • (ContinuousLinearMap.snd ℂ ℂ ℂ)) (z, τ) from this.cexp

Result:
n : ℤ
z τ : ℂ
f : ℂ × ℂ → ℂ := fun p => 2 * ↑π * I * ↑n * p.1 + ↑π * I * ↑n ^ 2 * p.2
⊢ HasFDerivAt f ((2 * ↑π * I * ↑n) • ContinuousLinearMap.fst ℂ ℂ ℂ + (↑π * I * ↑n ^ 2) • ContinuousLinearMap.snd ℂ ℂ ℂ)
    (z, τ)

Proof state:
n : ℤ
z τ : ℂ
⊢ HasFDerivAt (fun p => jacobiTheta₂_term n p.1 p.2) (jacobiTheta₂_term_fderiv n z τ) (z, τ)

Tactic:
let f : ℂ × ℂ → ℂ := fun p ↦ 2 * π * I * n * p.1 + π * I * n ^ 2 * p.2

Result:
n : ℤ
z τ : ℂ
f : ℂ × ℂ → ℂ := fun p => 2 * ↑π * I * ↑n * p.1 + ↑π * I * ↑n ^ 2 * p.2
⊢ HasFDerivAt (fun p => jacobiTheta₂_term n p.1 p.2) (jacobiTheta₂_term_fderiv n z τ) (z, τ)

Proof state:
n : ℤ
z τ : ℂ
f : ℂ × ℂ → ℂ := fun p => 2 * ↑π * I * ↑n * p.1 + ↑π * I * ↑n ^ 2 * p.2
⊢ HasFDerivAt f ((2 * ↑π * I * ↑n) • ContinuousLinearMap.fst ℂ ℂ ℂ + (↑π * I * ↑n ^ 2) • ContinuousLinearMap.snd ℂ ℂ ℂ)
    (z, τ)

Tactic:
exact (hasFDerivAt_fst.const_mul _).add (hasFDerivAt_snd.const_mul _)

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Exp.lean
theorem comap_exp_atTop : comap exp atTop = atTop

Proof state:
⊢ comap rexp atTop = atTop

Tactic:
rw [← map_exp_atTop, comap_map exp_injective, map_exp_atTop]

Result:
no goals
-- Mathlib/CategoryTheory/SmallObject/IsCardinalForSmallObjectArgument.lean
@[reassoc (attr := simp)]
lemma iterationFunctorObjObjRightIso_ιIteration_app_right (f : Arrow C) (j : κ.ord.toType) :
    (iterationFunctorObjObjRightIso I κ f j).hom ≫ ((ιIteration I κ).app f).right =
      (transfiniteCompositionOfShapeιIterationAppRight I κ f).incl.app j

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
I : MorphismProperty C
κ : Cardinal.{w}
inst✝² : Fact κ.IsRegular
inst✝¹ : OrderBot κ.ord.toType
inst✝ : I.IsCardinalForSmallObjectArgument κ
f : Arrow C
j : κ.ord.toType
⊢ (iterationFunctorObjObjRightIso I κ f j).hom ≫ ((ιIteration I κ).app f).right =
    (transfiniteCompositionOfShapeιIterationAppRight I κ f).incl.app j

Tactic:
simp [iterationFunctorObjObjRightIso, iterationObjRightIso]

Result:
no goals
-- Mathlib/Data/List/AList.lean
theorem union_assoc {s₁ s₂ s₃ : AList β} : (s₁ ∪ s₂ ∪ s₃).entries ~ (s₁ ∪ (s₂ ∪ s₃)).entries :=
  lookup_ext (AList.nodupKeys _) (AList.nodupKeys _)
    (by simp [not_or, or_assoc, and_or_left, and_assoc])

Proof state:
α : Type u
β : α → Type v
inst✝ : DecidableEq α
s₁ s₂ s₃ : AList β
⊢ ∀ (x : α) (y : β x), y ∈ dlookup x (s₁ ∪ s₂ ∪ s₃).entries ↔ y ∈ dlookup x (s₁ ∪ (s₂ ∪ s₃)).entries

Tactic:
simp [not_or, or_assoc, and_or_left, and_assoc]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem singleton_eq_append_iff :
    [x] = a ++ b ↔ (a = [] ∧ b = [x]) ∨ (a = [x] ∧ b = [])

Proof state:
α✝ : Type u_1
x : α✝
a b : List α✝
⊢ [x] = a ++ b ↔ a = [] ∧ b = [x] ∨ a = [x] ∧ b = []

Tactic:
cases a <;> cases b <;> simp [eq_comm]

Result:
no goals
-- Mathlib/Geometry/Manifold/IsManifold/Basic.lean
theorem target_eq : I.target = range (I : H → E)

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
⊢ I.target = range ↑I

Tactic:
rw [← image_univ, ← I.source_eq]

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
⊢ I.target = ↑I '' I.source

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
⊢ I.target = ↑I '' I.source

Tactic:
exact I.image_source_eq_target.symm

Result:
no goals
-- Mathlib/Analysis/BoxIntegral/Box/SubboxInduction.lean
theorem iUnion_coe_splitCenterBox (I : Box ι) : ⋃ s, (I.splitCenterBox s : Set (ι → ℝ)) = I

Proof state:
case h
ι : Type u_1
I : Box ι
x : ι → ℝ
⊢ x ∈ ⋃ s, ↑(I.splitCenterBox s) ↔ x ∈ ↑I

Tactic:
simp

Result:
no goals

Proof state:
ι : Type u_1
I : Box ι
⊢ ⋃ s, ↑(I.splitCenterBox s) = ↑I

Tactic:
ext x

Result:
case h
ι : Type u_1
I : Box ι
x : ι → ℝ
⊢ x ∈ ⋃ s, ↑(I.splitCenterBox s) ↔ x ∈ ↑I
-- Mathlib/RingTheory/Ideal/Cotangent.lean
theorem range_cotangentToQuotientSquare :
    LinearMap.range I.cotangentToQuotientSquare = I.cotangentIdeal.restrictScalars R

Proof state:
R : Type u
inst✝ : CommRing R
I : Ideal R
⊢ LinearMap.range (I.cotangentToQuotientSquare ∘ₗ I.toCotangent) = Submodule.restrictScalars R I.cotangentIdeal

Tactic:
rw [to_quotient_square_comp_toCotangent, LinearMap.range_comp, I.range_subtype]

Result:
R : Type u
inst✝ : CommRing R
I : Ideal R
⊢ Submodule.map (Submodule.mkQ (I ^ 2)) I = Submodule.restrictScalars R I.cotangentIdeal

Proof state:
R : Type u
inst✝ : CommRing R
I : Ideal R
⊢ Submodule.map (Submodule.mkQ (I ^ 2)) I = Submodule.restrictScalars R I.cotangentIdeal

Tactic:
ext

Result:
case h
R : Type u
inst✝ : CommRing R
I : Ideal R
x✝ : R ⧸ I ^ 2
⊢ x✝ ∈ Submodule.map (Submodule.mkQ (I ^ 2)) I ↔ x✝ ∈ Submodule.restrictScalars R I.cotangentIdeal

Proof state:
R : Type u
inst✝ : CommRing R
I : Ideal R
⊢ LinearMap.range I.cotangentToQuotientSquare = Submodule.restrictScalars R I.cotangentIdeal

Tactic:
trans LinearMap.range (I.cotangentToQuotientSquare.comp I.toCotangent)

Result:
R : Type u
inst✝ : CommRing R
I : Ideal R
⊢ LinearMap.range I.cotangentToQuotientSquare = LinearMap.range (I.cotangentToQuotientSquare ∘ₗ I.toCotangent)

R : Type u
inst✝ : CommRing R
I : Ideal R
⊢ LinearMap.range (I.cotangentToQuotientSquare ∘ₗ I.toCotangent) = Submodule.restrictScalars R I.cotangentIdeal

Proof state:
R : Type u
inst✝ : CommRing R
I : Ideal R
⊢ LinearMap.range I.cotangentToQuotientSquare = LinearMap.range (I.cotangentToQuotientSquare ∘ₗ I.toCotangent)

Tactic:
rw [LinearMap.range_comp, I.toCotangent_range, Submodule.map_top]

Result:
no goals

Proof state:
case h
R : Type u
inst✝ : CommRing R
I : Ideal R
x✝ : R ⧸ I ^ 2
⊢ x✝ ∈ Submodule.map (Submodule.mkQ (I ^ 2)) I ↔ x✝ ∈ Submodule.restrictScalars R I.cotangentIdeal

Tactic:
rfl

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem getD_erase_self [LawfulBEq α] (h : m.1.WF) {k : α} {fallback : β k} :
    (m.erase k).getD k fallback = fallback

Proof state:
α : Type u
β : α → Type v
m : Raw₀ α β
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
h : m.val.WF
k : α
fallback : β k
⊢ (m.erase k).getD k fallback = fallback

Tactic:
simp_to_model [erase] using List.getValueCastD_eraseKey_self

Result:
no goals
-- Mathlib/Analysis/BoxIntegral/Box/Basic.lean
theorem injective_coe : Injective ((↑) : Box ι → Set (ι → ℝ))

Proof state:
case mk.mk.e_lower
ι : Type u_1
l₁ u₁ : ι → ℝ
h₁ : ∀ (i : ι), l₁ i < u₁ i
l₂ u₂ : ι → ℝ
h₂ : ∀ (i : ι), l₂ i < u₂ i
h : (l₂ ≤ l₁ ∧ u₁ ≤ u₂) ∧ l₁ ≤ l₂ ∧ u₂ ≤ u₁
⊢ l₁ = l₂

case mk.mk.e_upper
ι : Type u_1
l₁ u₁ : ι → ℝ
h₁ : ∀ (i : ι), l₁ i < u₁ i
l₂ u₂ : ι → ℝ
h₂ : ∀ (i : ι), l₂ i < u₂ i
h : (l₂ ≤ l₁ ∧ u₁ ≤ u₂) ∧ l₁ ≤ l₂ ∧ u₂ ≤ u₁
⊢ u₁ = u₂

Tactic:
exacts [le_antisymm h.2.1 h.1.1, le_antisymm h.1.2 h.2.2]

Result:
no goals

Proof state:
case mk.mk
ι : Type u_1
l₁ u₁ : ι → ℝ
h₁ : ∀ (i : ι), l₁ i < u₁ i
l₂ u₂ : ι → ℝ
h₂ : ∀ (i : ι), l₂ i < u₂ i
h : (l₂ ≤ l₁ ∧ u₁ ≤ u₂) ∧ l₁ ≤ l₂ ∧ u₂ ≤ u₁
⊢ { lower := l₁, upper := u₁, lower_lt_upper := h₁ } = { lower := l₂, upper := u₂, lower_lt_upper := h₂ }

Tactic:
congr

Result:
case mk.mk.e_lower
ι : Type u_1
l₁ u₁ : ι → ℝ
h₁ : ∀ (i : ι), l₁ i < u₁ i
l₂ u₂ : ι → ℝ
h₂ : ∀ (i : ι), l₂ i < u₂ i
h : (l₂ ≤ l₁ ∧ u₁ ≤ u₂) ∧ l₁ ≤ l₂ ∧ u₂ ≤ u₁
⊢ l₁ = l₂

case mk.mk.e_upper
ι : Type u_1
l₁ u₁ : ι → ℝ
h₁ : ∀ (i : ι), l₁ i < u₁ i
l₂ u₂ : ι → ℝ
h₂ : ∀ (i : ι), l₂ i < u₂ i
h : (l₂ ≤ l₁ ∧ u₁ ≤ u₂) ∧ l₁ ≤ l₂ ∧ u₂ ≤ u₁
⊢ u₁ = u₂

Proof state:
case mk.mk
ι : Type u_1
l₁ u₁ : ι → ℝ
h₁ : ∀ (i : ι), l₁ i < u₁ i
l₂ u₂ : ι → ℝ
h₂ : ∀ (i : ι), l₂ i < u₂ i
h : ↑{ lower := l₁, upper := u₁, lower_lt_upper := h₁ } = ↑{ lower := l₂, upper := u₂, lower_lt_upper := h₂ }
⊢ { lower := l₁, upper := u₁, lower_lt_upper := h₁ } = { lower := l₂, upper := u₂, lower_lt_upper := h₂ }

Tactic:
simp only [Subset.antisymm_iff, coe_subset_coe, le_iff_bounds] at h

Result:
case mk.mk
ι : Type u_1
l₁ u₁ : ι → ℝ
h₁ : ∀ (i : ι), l₁ i < u₁ i
l₂ u₂ : ι → ℝ
h₂ : ∀ (i : ι), l₂ i < u₂ i
h : (l₂ ≤ l₁ ∧ u₁ ≤ u₂) ∧ l₁ ≤ l₂ ∧ u₂ ≤ u₁
⊢ { lower := l₁, upper := u₁, lower_lt_upper := h₁ } = { lower := l₂, upper := u₂, lower_lt_upper := h₂ }

Proof state:
ι : Type u_1
⊢ Injective toSet

Tactic:
rintro ⟨l₁, u₁, h₁⟩ ⟨l₂, u₂, h₂⟩ h

Result:
case mk.mk
ι : Type u_1
l₁ u₁ : ι → ℝ
h₁ : ∀ (i : ι), l₁ i < u₁ i
l₂ u₂ : ι → ℝ
h₂ : ∀ (i : ι), l₂ i < u₂ i
h : ↑{ lower := l₁, upper := u₁, lower_lt_upper := h₁ } = ↑{ lower := l₂, upper := u₂, lower_lt_upper := h₂ }
⊢ { lower := l₁, upper := u₁, lower_lt_upper := h₁ } = { lower := l₂, upper := u₂, lower_lt_upper := h₂ }