harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Group/Basic.lean
theorem mul_eq_one_iff_inv_eq : a * b = 1 ↔ a⁻¹ = b

Proof state:
G : Type u_3
inst✝ : Group G
a b : G
⊢ a * b = 1 ↔ a⁻¹ = b

Tactic:
rw [mul_eq_one_iff_eq_inv, inv_eq_iff_eq_inv]

Result:
no goals
-- Mathlib/Algebra/Order/Interval/Set/Instances.lean
theorem one_sub_nonneg (x : Icc (0 : β) 1) : 0 ≤ 1 - (x : β)

Proof state:
β : Type u_2
inst✝ : OrderedRing β
x : ↑(Icc 0 1)
⊢ 0 ≤ 1 - ↑x

Tactic:
simpa using x.2.2

Result:
no goals
-- Mathlib/Algebra/MvPolynomial/Cardinal.lean
theorem cardinalMk_eq_max [Nonempty σ] [Nontrivial R] :
    #(MvPolynomial σ R) = max (max #R #σ) ℵ₀

Proof state:
σ R : Type u
inst✝² : CommSemiring R
inst✝¹ : Nonempty σ
inst✝ : Nontrivial R
⊢ #(MvPolynomial σ R) = #R ⊔ #σ ⊔ ℵ₀

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/SpecificLimits/Basic.lean
theorem NNReal.tendsto_pow_atTop_nhds_zero_of_lt_one {r : ℝ≥0} (hr : r < 1) :
    Tendsto (fun n : ℕ ↦ r ^ n) atTop (𝓝 0) :=
  NNReal.tendsto_coe.1 <| by
    simp only [NNReal.coe_pow, NNReal.coe_zero,
      _root_.tendsto_pow_atTop_nhds_zero_of_lt_one r.coe_nonneg hr]

Proof state:
r : ℝ≥0
hr : r < 1
⊢ Tendsto (fun a => ↑(r ^ a)) atTop (𝓝 ↑0)

Tactic:
simp only [NNReal.coe_pow, NNReal.coe_zero,
  _root_.tendsto_pow_atTop_nhds_zero_of_lt_one r.coe_nonneg hr]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/Raw.lean
theorem getKey?_val [BEq α] [Hashable α] {m : Raw₀ α β} {a : α} :
    m.val.getKey? a = m.getKey? a

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : Hashable α
m : Raw₀ α β
a : α
⊢ m.val.getKey? a = m.getKey? a

Tactic:
simp [Raw.getKey?, m.2]

Result:
no goals
-- Mathlib/Order/UpperLower/Basic.lean
theorem OrderEmbedding.image_Ici (e : α ↪o β) (he : IsUpperSet (range e)) (a : α) :
    e '' Ici a = Ici (e a)

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : Preorder α
inst✝ : Preorder β
e : α ↪o β
he : IsUpperSet (range ⇑e)
a : α
⊢ ⇑e '' Ici a = Ici (e a)

Tactic:
rw [← e.preimage_Ici, image_preimage_eq_inter_range,
  inter_eq_left.2 <| he.Ici_subset (mem_range_self _)]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/SimpLemmas.lean
theorem Bool.and_self (b : Bool) : (b && b) = b

Proof state:
b : Bool
⊢ (b && b) = b

Tactic:
cases b <;> rfl

Result:
no goals
-- Mathlib/Data/Nat/GCD/BigOperators.lean
theorem coprime_list_prod_right_iff {k : ℕ} {l : List ℕ} :
    Coprime k l.prod ↔ ∀ n ∈ l, Coprime k n

Proof state:
k : ℕ
l : List ℕ
⊢ k.Coprime l.prod ↔ ∀ n ∈ l, k.Coprime n

Tactic:
simp_rw [coprime_comm (n := k), coprime_list_prod_left_iff]

Result:
no goals
-- Mathlib/Topology/MetricSpace/Contracting.lean
theorem edist_efixedPoint_le' {s : Set α} (hsc : IsComplete s) (hsf : MapsTo f s s)
    (hf : ContractingWith K <| hsf.restrict f s s) {x : α} (hxs : x ∈ s) (hx : edist x (f x) ≠ ∞) :
    edist x (efixedPoint' f hsc hsf hf x hxs hx) ≤ edist x (f x) / (1 - K)

Proof state:
case h.e'_4.h.e'_5
α : Type u_1
inst✝ : EMetricSpace α
K : ℝ≥0
f : α → α
s : Set α
hsc : IsComplete s
hsf : MapsTo f s s
hf : ContractingWith K (MapsTo.restrict f s s hsf)
x : α
hxs : x ∈ s
hx : edist x (f x) ≠ ⊤
⊢ edist x (f x) = edist x (f x) * ↑K ^ 0

Tactic:
rw [pow_zero, mul_one]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : EMetricSpace α
K : ℝ≥0
f : α → α
s : Set α
hsc : IsComplete s
hsf : MapsTo f s s
hf : ContractingWith K (MapsTo.restrict f s s hsf)
x : α
hxs : x ∈ s
hx : edist x (f x) ≠ ⊤
⊢ edist x (efixedPoint' f hsc hsf hf x hxs hx) ≤ edist x (f x) / (1 - ↑K)

Tactic:
convert hf.apriori_edist_iterate_efixedPoint_le' hsc hsf hxs hx 0

Result:
case h.e'_4.h.e'_5
α : Type u_1
inst✝ : EMetricSpace α
K : ℝ≥0
f : α → α
s : Set α
hsc : IsComplete s
hsf : MapsTo f s s
hf : ContractingWith K (MapsTo.restrict f s s hsf)
x : α
hxs : x ∈ s
hx : edist x (f x) ≠ ⊤
⊢ edist x (f x) = edist x (f x) * ↑K ^ 0
-- Mathlib/CategoryTheory/Sites/IsSheafOneHypercover.lean
lemma hom_ext [H.IsGenerating] {X : C} (S : Sieve X) (hS : S ∈ J X) {T : A}
    {x y : T ⟶ P.obj (Opposite.op X)}
    (h : ∀ ⦃Y : C⦄ (f : Y ⟶ X) (_ : S f), x ≫ P.map f.op = y ≫ P.map f.op) :
    x = y

Proof state:
case intro.intro
C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝¹ : Category.{v', u'} A
H : J.OneHypercoverFamily
P : Cᵒᵖ ⥤ A
hP : ∀ ⦃X : C⦄ (E : J.OneHypercover X), H E → Nonempty (IsLimit (E.multifork P))
inst✝ : H.IsGenerating
X : C
S : Sieve X
hS : S ∈ J X
T : A
x y : T ⟶ P.obj (Opposite.op X)
h : ∀ ⦃Y : C⦄ (f : Y ⟶ X), S.arrows f → x ≫ P.map f.op = y ≫ P.map f.op
E : J.OneHypercover X
hE : H E
le : E.sieve₀ ≤ S
⊢ x = y

Tactic:
exact Multifork.IsLimit.hom_ext (hP E hE).some (fun j => h _ (le _ (Sieve.ofArrows_mk _ _ _)))

Result:
no goals

Proof state:
C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝¹ : Category.{v', u'} A
H : J.OneHypercoverFamily
P : Cᵒᵖ ⥤ A
hP : ∀ ⦃X : C⦄ (E : J.OneHypercover X), H E → Nonempty (IsLimit (E.multifork P))
inst✝ : H.IsGenerating
X : C
S : Sieve X
hS : S ∈ J X
T : A
x y : T ⟶ P.obj (Opposite.op X)
h : ∀ ⦃Y : C⦄ (f : Y ⟶ X), S.arrows f → x ≫ P.map f.op = y ≫ P.map f.op
⊢ x = y

Tactic:
obtain ⟨E, hE, le⟩ := H.exists_oneHypercover S hS

Result:
case intro.intro
C : Type u
inst✝² : Category.{v, u} C
J : GrothendieckTopology C
A : Type u'
inst✝¹ : Category.{v', u'} A
H : J.OneHypercoverFamily
P : Cᵒᵖ ⥤ A
hP : ∀ ⦃X : C⦄ (E : J.OneHypercover X), H E → Nonempty (IsLimit (E.multifork P))
inst✝ : H.IsGenerating
X : C
S : Sieve X
hS : S ∈ J X
T : A
x y : T ⟶ P.obj (Opposite.op X)
h : ∀ ⦃Y : C⦄ (f : Y ⟶ X), S.arrows f → x ≫ P.map f.op = y ≫ P.map f.op
E : J.OneHypercover X
hE : H E
le : E.sieve₀ ≤ S
⊢ x = y
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem toInt_or (x y : BitVec w) :
    BitVec.toInt (x ||| y) = Int.bmod (BitVec.toNat x ||| BitVec.toNat y) (2^w)

Proof state:
w : Nat
x y : BitVec w
⊢ (x ||| y).toInt = (↑(x.toNat ||| y.toNat)).bmod (2 ^ w)

Tactic:
rw_mod_cast [Int.bmod_def, BitVec.toInt, toNat_or, Nat.mod_eq_of_lt
  (Nat.or_lt_two_pow (BitVec.isLt x) (BitVec.isLt y))]

Result:
w : Nat
x y : BitVec w
⊢ (if 2 * (x.toNat ||| y.toNat) < 2 ^ w then ↑(x.toNat ||| y.toNat) else ↑(x.toNat ||| y.toNat) - ↑(2 ^ w)) =
    if x.toNat ||| y.toNat < (2 ^ w + 1) / 2 then ↑(x.toNat ||| y.toNat) else ↑(x.toNat ||| y.toNat) - ↑(2 ^ w)

Proof state:
w : Nat
x y : BitVec w
⊢ (if 2 * (x.toNat ||| y.toNat) < 2 ^ w then ↑(x.toNat ||| y.toNat) else ↑(x.toNat ||| y.toNat) - ↑(2 ^ w)) =
    if x.toNat ||| y.toNat < (2 ^ w + 1) / 2 then ↑(x.toNat ||| y.toNat) else ↑(x.toNat ||| y.toNat) - ↑(2 ^ w)

Tactic:
omega

Result:
no goals
-- Mathlib/NumberTheory/Divisors.lean
theorem card_divisors_le_self (n : ℕ) : #n.divisors ≤ n := calc
  _ ≤ #(Ico 1 (n + 1))

Proof state:
case a
n : ℕ
⊢ n.divisors ⊆ Ico 1 (n + 1)

Tactic:
simp only [divisors, filter_subset]

Result:
no goals

Proof state:
n : ℕ
⊢ #(Ico 1 (n + 1)) = n

Tactic:
rw [card_Ico, add_tsub_cancel_right]

Result:
no goals

Proof state:
n : ℕ
⊢ #n.divisors ≤ #(Ico 1 (n + 1))

Tactic:
apply card_le_card

Result:
case a
n : ℕ
⊢ n.divisors ⊆ Ico 1 (n + 1)
-- Mathlib/Analysis/Normed/Field/InfiniteSum.lean
theorem summable_norm_sum_mul_range_of_summable_norm {f g : ℕ → R} (hf : Summable fun x => ‖f x‖)
    (hg : Summable fun x => ‖g x‖) : Summable fun n => ‖∑ k ∈ range (n + 1), f k * g (n - k)‖

Proof state:
R : Type u_1
inst✝ : NormedRing R
f g : ℕ → R
hf : Summable fun x => ‖f x‖
hg : Summable fun x => ‖g x‖
⊢ Summable fun n => ‖∑ k ∈ range (n + 1), f k * g (n - k)‖

Tactic:
simp_rw [← sum_antidiagonal_eq_sum_range_succ fun k l => f k * g l]

Result:
R : Type u_1
inst✝ : NormedRing R
f g : ℕ → R
hf : Summable fun x => ‖f x‖
hg : Summable fun x => ‖g x‖
⊢ Summable fun n => ‖∑ ij ∈ antidiagonal n, f ij.1 * g ij.2‖

Proof state:
R : Type u_1
inst✝ : NormedRing R
f g : ℕ → R
hf : Summable fun x => ‖f x‖
hg : Summable fun x => ‖g x‖
⊢ Summable fun n => ‖∑ ij ∈ antidiagonal n, f ij.1 * g ij.2‖

Tactic:
exact summable_norm_sum_mul_antidiagonal_of_summable_norm hf hg

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Weierstrass.lean
/-- A variant of `WeierstrassCurve.j_eq_zero_iff_of_char_two` without assuming a reduced ring. -/
lemma j_eq_zero_iff_of_char_two' : W.j = 0 ↔ W.a₁ ^ 12 = 0

Proof state:
R : Type u
inst✝² : CommRing R
W : WeierstrassCurve R
inst✝¹ : W.IsElliptic
inst✝ : CharP R 2
⊢ W.j = 0 ↔ W.a₁ ^ 12 = 0

Tactic:
rw [j_of_char_two, Units.mul_right_eq_zero]

Result:
no goals
-- Mathlib/RingTheory/Localization/Defs.lean
theorem mk'_neg (x : R) (y : M) :
    mk' S (-x) y = - mk' S x y

Proof state:
R : Type u_1
inst✝³ : CommRing R
M : Submonoid R
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
x : R
y : ↥M
⊢ mk' S (-x) y = -mk' S x y

Tactic:
rw [eq_comm, eq_mk'_iff_mul_eq, neg_mul, map_neg, mk'_spec]

Result:
no goals
-- Mathlib/Order/Heyting/Hom.lean
theorem map_compl (a : α) : f aᶜ = (f a)ᶜ

Proof state:
F : Type u_1
α : Type u_2
β : Type u_3
inst✝³ : FunLike F α β
inst✝² : HeytingAlgebra α
inst✝¹ : HeytingAlgebra β
inst✝ : HeytingHomClass F α β
f : F
a : α
⊢ f aᶜ = (f a)ᶜ

Tactic:
rw [← himp_bot, ← himp_bot, map_himp, map_bot]

Result:
no goals
-- Mathlib/RingTheory/Jacobson/Radical.lean
theorem comap_jacobson_of_bijective (hf : Function.Bijective f) :
    comap f (jacobson R₂ M₂) = jacobson R M :=
  comap_jacobson_of_ker_le hf.2 <| by simp_rw [(LinearMapClass.ker_eq_bot _).mpr hf.1, bot_le]

Proof state:
R : Type u_1
R₂ : Type u_2
M : Type u_3
M₂ : Type u_4
inst✝⁸ : Ring R
inst✝⁷ : Ring R₂
inst✝⁶ : AddCommGroup M
inst✝⁵ : Module R M
inst✝⁴ : AddCommGroup M₂
inst✝³ : Module R₂ M₂
τ₁₂ : R →+* R₂
inst✝² : RingHomSurjective τ₁₂
F : Type u_5
inst✝¹ : FunLike F M M₂
inst✝ : SemilinearMapClass F τ₁₂ M M₂
f : F
hf : Function.Bijective ⇑f
⊢ LinearMap.ker f ≤ jacobson R M

Tactic:
simp_rw [(LinearMapClass.ker_eq_bot _).mpr hf.1, bot_le]

Result:
no goals
-- Mathlib/LinearAlgebra/RootSystem/Finite/CanonicalBilinear.lean
@[simp]
lemma rootForm_reflection_reflection_apply (i : ι) (x y : M) :
    P.RootForm (P.reflection i x) (P.reflection i y) = P.RootForm x y

Proof state:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
P : RootPairing ι R M N
inst✝ : Fintype ι
i : ι
x y : M
⊢ ∑ x_1 : ι, (P.coroot' ((P.reflection_perm i) x_1)) x * (P.coroot' ((P.reflection_perm i) x_1)) y =
    ∑ i : ι, (P.coroot' i) x * (P.coroot' i) y

Tactic:
exact Fintype.sum_equiv (P.reflection_perm i)
  (fun j ↦ (P.coroot' (P.reflection_perm i j) x) * (P.coroot' (P.reflection_perm i j) y))
  (fun j ↦ P.coroot' j x * P.coroot' j y) (congrFun rfl)

Result:
no goals

Proof state:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
P : RootPairing ι R M N
inst✝ : Fintype ι
i : ι
x y : M
⊢ (P.RootForm ((P.reflection i) x)) ((P.reflection i) y) = (P.RootForm x) y

Tactic:
simp only [rootForm_apply_apply, coroot'_reflection]

Result:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : AddCommGroup N
inst✝¹ : Module R N
P : RootPairing ι R M N
inst✝ : Fintype ι
i : ι
x y : M
⊢ ∑ x_1 : ι, (P.coroot' ((P.reflection_perm i) x_1)) x * (P.coroot' ((P.reflection_perm i) x_1)) y =
    ∑ i : ι, (P.coroot' i) x * (P.coroot' i) y
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Attach.lean
theorem reverse_attachWith {P : α → Prop} {xs : List α}
    {H : ∀ (a : α), a ∈ xs → P a} :
    (xs.attachWith P H).reverse = (xs.reverse.attachWith P (fun a h => H a (by simpa using h))) :=
  reverse_pmap ..

Proof state:
α : Type ?u.78411
P : α → Prop
xs : List α
H : ∀ (a : α), a ∈ xs → P a
a : α
h : a ∈ xs.reverse
⊢ a ∈ xs

Tactic:
simpa using h

Result:
no goals
-- Mathlib/FieldTheory/Minpoly/Field.lean
theorem coeff_zero_ne_zero (hx : IsIntegral A x) (h : x ≠ 0) : coeff (minpoly A x) 0 ≠ 0

Proof state:
A : Type u_1
B : Type u_2
inst✝³ : Field A
inst✝² : Ring B
inst✝¹ : IsDomain B
inst✝ : Algebra A B
x : B
hx : IsIntegral A x
h : (minpoly A x).coeff 0 = 0
⊢ x = 0

Tactic:
simpa only [hx, coeff_zero_eq_zero] using h

Result:
no goals

Proof state:
A : Type u_1
B : Type u_2
inst✝³ : Field A
inst✝² : Ring B
inst✝¹ : IsDomain B
inst✝ : Algebra A B
x : B
hx : IsIntegral A x
h : x ≠ 0
⊢ (minpoly A x).coeff 0 ≠ 0

Tactic:
contrapose! h

Result:
A : Type u_1
B : Type u_2
inst✝³ : Field A
inst✝² : Ring B
inst✝¹ : IsDomain B
inst✝ : Algebra A B
x : B
hx : IsIntegral A x
h : (minpoly A x).coeff 0 = 0
⊢ x = 0
-- Mathlib/NumberTheory/PythagoreanTriples.lean
theorem coprime_sq_sub_mul {m n : ℤ} (h : Int.gcd m n = 1)
    (hmn : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0) :
    Int.gcd (m ^ 2 - n ^ 2) (2 * m * n) = 1

Proof state:
case inr
m n : ℤ
h : m.gcd n = 1
h2 : m % 2 = 1 ∧ n % 2 = 0
⊢ (m ^ 2 - n ^ 2).gcd (2 * m * n) = 1

Tactic:
exact coprime_sq_sub_mul_of_odd_even h h2.left h2.right

Result:
no goals

Proof state:
case inl
m n : ℤ
h : m.gcd n = 1
h1 : m % 2 = 0 ∧ n % 2 = 1
⊢ (m ^ 2 - n ^ 2).gcd (2 * m * n) = 1

Tactic:
exact coprime_sq_sub_mul_of_even_odd h h1.left h1.right

Result:
no goals

Proof state:
m n : ℤ
h : m.gcd n = 1
hmn : m % 2 = 0 ∧ n % 2 = 1 ∨ m % 2 = 1 ∧ n % 2 = 0
⊢ (m ^ 2 - n ^ 2).gcd (2 * m * n) = 1

Tactic:
rcases hmn with h1 | h2

Result:
case inl
m n : ℤ
h : m.gcd n = 1
h1 : m % 2 = 0 ∧ n % 2 = 1
⊢ (m ^ 2 - n ^ 2).gcd (2 * m * n) = 1

case inr
m n : ℤ
h : m.gcd n = 1
h2 : m % 2 = 1 ∧ n % 2 = 0
⊢ (m ^ 2 - n ^ 2).gcd (2 * m * n) = 1
-- Mathlib/RingTheory/PolynomialAlgebra.lean
theorem matPolyEquiv_diagonal_X :
    matPolyEquiv (diagonal fun _ : n => (X : R[X])) = X

Proof state:
R : Type u_1
inst✝² : CommSemiring R
n : Type w
inst✝¹ : DecidableEq n
inst✝ : Fintype n
⊢ matPolyEquiv (diagonal fun x => X) = X

Tactic:
rw [← matPolyEquiv_symm_X, AlgEquiv.apply_symm_apply]

Result:
no goals
-- Mathlib/Logic/Denumerable.lean
theorem succ_le_of_lt {x y : s} (h : y < x) : succ y ≤ x :=
  have hx : ∃ m, (y : ℕ) + m + 1 ∈ s := exists_succ _
  let ⟨k, hk⟩ := Nat.exists_eq_add_of_lt h
  have : Nat.find hx ≤ k := Nat.find_min' _ (hk ▸ x.2)
  show (y : ℕ) + Nat.find hx + 1 ≤ x by omega

Proof state:
s : Set ℕ
inst✝¹ : Infinite ↑s
inst✝ : DecidablePred fun x => x ∈ s
x y : ↑s
h : y < x
hx : ∃ m, ↑y + m + 1 ∈ s
k : ℕ
hk : ↑x = ↑y + k + 1
this : Nat.find hx ≤ k
⊢ ↑y + Nat.find hx + 1 ≤ ↑x

Tactic:
omega

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem contains_of_contains_insertMany_list [EquivBEq α] [LawfulHashable α] (h : m.1.WF)
    {l : List ( α × β )} {k : α} :
    (insertMany m l).1.contains k → (l.map Prod.fst).contains k = false → m.contains k

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

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

Result:
no goals
-- Mathlib/GroupTheory/Finiteness.lean
theorem Submonoid.fg_iff_add_fg (P : Submonoid M) : P.FG ↔ P.toAddSubmonoid.FG :=
  ⟨fun h =>
    let ⟨S, hS, hf⟩ := (Submonoid.fg_iff _).1 h
    (AddSubmonoid.fg_iff _).mpr
      ⟨Additive.toMul ⁻¹' S, by simp [← Submonoid.toAddSubmonoid_closure, hS], hf⟩,
    fun h =>
    let ⟨T, hT, hf⟩ := (AddSubmonoid.fg_iff _).1 h
    (Submonoid.fg_iff _).mpr
      ⟨Multiplicative.ofAdd ⁻¹' T, by simp [← AddSubmonoid.toSubmonoid'_closure, hT], hf⟩⟩

Proof state:
M : Type u_1
inst✝ : Monoid M
P : Submonoid M
h : P.FG
S : Set M
hS : closure S = P
hf : S.Finite
⊢ AddSubmonoid.closure (⇑Additive.toMul ⁻¹' S) = toAddSubmonoid P

Tactic:
simp [← Submonoid.toAddSubmonoid_closure, hS]

Result:
no goals

Proof state:
M : Type u_1
inst✝ : Monoid M
P : Submonoid M
h : (toAddSubmonoid P).FG
T : Set (Additive M)
hT : AddSubmonoid.closure T = toAddSubmonoid P
hf : T.Finite
⊢ closure (⇑Multiplicative.ofAdd ⁻¹' T) = P

Tactic:
simp [← AddSubmonoid.toSubmonoid'_closure, hT]

Result:
no goals
-- Mathlib/NumberTheory/LSeries/Dirichlet.lean
/-- The convolution of a Dirichlet character `χ` with the twist `χ * μ` is `δ`,
the indicator function of `{1}`. -/
lemma convolution_mul_moebius {n : ℕ} (χ : DirichletCharacter ℂ n) : ↗χ ⍟ (↗χ * ↗μ) = δ

Proof state:
n : ℕ
χ : DirichletCharacter ℂ n
this : (1 ⍟ fun x => ↑(μ x)) = δ
⊢ (fun n_1 => χ ↑n_1) * 1 ⍟ ((fun n_1 => χ ↑n_1) * fun n => ↑(μ n)) = δ

Tactic:
simpa only [mul_convolution_distrib χ 1 ↗μ, this] using mul_delta _

Result:
no goals

Proof state:
n : ℕ
χ : DirichletCharacter ℂ n
⊢ (1 ⍟ fun x => ↑(μ x)) = δ

Tactic:
rw [one_convolution_eq_zeta_convolution, ← one_eq_delta]

Result:
n : ℕ
χ : DirichletCharacter ℂ n
⊢ ((fun x => ↑(ζ x)) ⍟ fun x => ↑(μ x)) = fun n => 1 n

Proof state:
n : ℕ
χ : DirichletCharacter ℂ n
this : (1 ⍟ fun x => ↑(μ x)) = δ
⊢ (fun n_1 => χ ↑n_1) ⍟ ((fun n_1 => χ ↑n_1) * fun n => ↑(μ n)) = δ

Tactic:
nth_rewrite 1 [← mul_one ↗χ]

Result:
n : ℕ
χ : DirichletCharacter ℂ n
this : (1 ⍟ fun x => ↑(μ x)) = δ
⊢ (fun n_1 => χ ↑n_1) * 1 ⍟ ((fun n_1 => χ ↑n_1) * fun n => ↑(μ n)) = δ

Proof state:
n : ℕ
χ : DirichletCharacter ℂ n
⊢ ((fun x => ↑(ζ x)) ⍟ fun x => ↑(μ x)) = fun n => 1 n

Tactic:
simp_rw [← natCoe_apply, ← intCoe_apply, coe_mul, coe_zeta_mul_coe_moebius]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Fin/Lemmas.lean
theorem one_mul (k : Fin (n + 1)) : (1 : Fin (n + 1)) * k = k

Proof state:
n : Nat
k : Fin (n + 1)
⊢ 1 * k = k

Tactic:
rw [Fin.mul_comm, Fin.mul_one]

Result:
no goals
-- Mathlib/Topology/Sets/Opens.lean
theorem not_nonempty_iff_eq_bot (U : Opens α) : ¬Set.Nonempty (U : Set α) ↔ U = ⊥

Proof state:
α : Type u_2
inst✝ : TopologicalSpace α
U : Opens α
⊢ ¬(↑U).Nonempty ↔ U = ⊥

Tactic:
rw [← coe_inj, coe_bot, ← Set.not_nonempty_iff_eq_empty]

Result:
no goals
-- Mathlib/RepresentationTheory/Character.lean
theorem average_char_eq_finrank_invariants (V : FDRep k G) :
    ⅟ (Fintype.card G : k) • ∑ g : G, V.character g = finrank k (invariants V.ρ)

Proof state:
k : Type u
inst✝³ : Field k
G : Type u
inst✝² : Group G
inst✝¹ : Fintype G
inst✝ : Invertible ↑(Fintype.card G)
V : FDRep k G
⊢ ⅟↑(Fintype.card G) • ∑ g : G, V.character g = (trace k ↑V.V) (averageMap V.ρ)

Tactic:
simp [character, GroupAlgebra.average, _root_.map_sum]

Result:
no goals

Proof state:
k : Type u
inst✝³ : Field k
G : Type u
inst✝² : Group G
inst✝¹ : Fintype G
inst✝ : Invertible ↑(Fintype.card G)
V : FDRep k G
⊢ ⅟↑(Fintype.card G) • ∑ g : G, V.character g = ↑(finrank k ↥(invariants V.ρ))

Tactic:
rw [← (isProj_averageMap V.ρ).trace]

Result:
k : Type u
inst✝³ : Field k
G : Type u
inst✝² : Group G
inst✝¹ : Fintype G
inst✝ : Invertible ↑(Fintype.card G)
V : FDRep k G
⊢ ⅟↑(Fintype.card G) • ∑ g : G, V.character g = (trace k ↑V.V) (averageMap V.ρ)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Lemmas.lean
theorem exists_eq_add_of_lt (h : m < n) : ∃ k : Nat, n = m + k + 1 :=
  ⟨n - (m + 1), by rw [Nat.add_right_comm, add_sub_of_le h]⟩

Proof state:
m n : Nat
h : m < n
⊢ n = m + (n - (m + 1)) + 1

Tactic:
rw [Nat.add_right_comm, add_sub_of_le h]

Result:
no goals
-- Mathlib/Order/Category/BddOrd.lean
lemma inv_hom_apply {X Y : BddOrd} (e : X ≅ Y) (x : X) : e.inv (e.hom x) = x

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

Tactic:
simp

Result:
no goals
-- Mathlib/FieldTheory/RatFunc/Basic.lean
theorem ofFractionRing_algebraMap (x : K[X]) :
    ofFractionRing (algebraMap _ (FractionRing K[X]) x) = algebraMap _ _ x

Proof state:
K : Type u
inst✝¹ : CommRing K
inst✝ : IsDomain K
x : K[X]
⊢ { toFractionRing := (algebraMap K[X] (FractionRing K[X])) x } = (algebraMap K[X] (RatFunc K)) x

Tactic:
rw [← mk_one, mk_one']

Result:
no goals
-- Mathlib/Analysis/RCLike/Basic.lean
theorem natCast_im (n : ℕ) : im (n : K) = 0

Proof state:
K : Type u_1
inst✝ : RCLike K
n : ℕ
⊢ im ↑n = 0

Tactic:
rw [← ofReal_natCast, ofReal_im]

Result:
no goals
-- Mathlib/CategoryTheory/ComposableArrows.lean
lemma map_id (i : Fin 2) : map f i i (by simp) = 𝟙 _ :=
  match i with
    | 0 => rfl
    | 1 => rfl

Proof state:
C : Type u_1
inst✝ : Category.{?u.10884, u_1} C
n m : ℕ
F G : ComposableArrows C n
X₀ X₁ : C
f : X₀ ⟶ X₁
i : Fin 2
⊢ i ≤ i

Tactic:
simp

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Connectivity/Subgraph.lean
theorem toSubgraph_adj_snd {u v} (w : G.Walk u v) (h : ¬ w.Nil) : w.toSubgraph.Adj u w.snd

Proof state:
V : Type u
G : SimpleGraph V
u v : V
w : G.Walk u v
h : ¬w.Nil
⊢ w.toSubgraph.Adj u w.snd

Tactic:
simpa using w.toSubgraph_adj_getVert (not_nil_iff_lt_length.mp h)

Result:
no goals
-- Mathlib/Data/Matrix/RowCol.lean
theorem row_injective [Nonempty ι] : Function.Injective (row ι : (n → α) → Matrix ι n α)

Proof state:
n : Type u_3
α : Type v
ι : Type u_6
inst✝ : Nonempty ι
⊢ Function.Injective (row ι)

Tactic:
inhabit ι

Result:
n : Type u_3
α : Type v
ι : Type u_6
inst✝ : Nonempty ι
inhabited_h : Inhabited ι
⊢ Function.Injective (row ι)

Proof state:
n : Type u_3
α : Type v
ι : Type u_6
inst✝ : Nonempty ι
inhabited_h : Inhabited ι
⊢ Function.Injective (row ι)

Tactic:
exact fun _x _y h => funext fun j => congr_fun₂ h default j

Result:
no goals
-- Mathlib/Geometry/Manifold/MFDeriv/Basic.lean
theorem mdifferentiableWithinAt_inter' (ht : t ∈ 𝓝[s] x) :
    MDifferentiableWithinAt I I' f (s ∩ t) x ↔ MDifferentiableWithinAt I I' 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
E' : Type u_5
inst✝⁴ : NormedAddCommGroup E'
inst✝³ : NormedSpace 𝕜 E'
H' : Type u_6
inst✝² : TopologicalSpace H'
I' : ModelWithCorners 𝕜 E' H'
M' : Type u_7
inst✝¹ : TopologicalSpace M'
inst✝ : ChartedSpace H' M'
f : M → M'
x : M
s t : Set M
ht : t ∈ 𝓝[s] x
⊢ MDifferentiableWithinAt I I' f (s ∩ t) x ↔ MDifferentiableWithinAt I I' f s x

Tactic:
rw [MDifferentiableWithinAt, MDifferentiableWithinAt,
  differentiableWithinAt_localInvariantProp.liftPropWithinAt_inter' ht]

Result:
no goals
-- Mathlib/Data/Complex/Exponential.lean
theorem exp_int_mul (z : ℂ) (n : ℤ) : Complex.exp (n * z) = Complex.exp z ^ n

Proof state:
z : ℂ
n : ℤ
⊢ cexp (↑n * z) = cexp z ^ n

Tactic:
cases n

Result:
case ofNat
z : ℂ
a✝ : ℕ
⊢ cexp (↑(Int.ofNat a✝) * z) = cexp z ^ Int.ofNat a✝

case negSucc
z : ℂ
a✝ : ℕ
⊢ cexp (↑(Int.negSucc a✝) * z) = cexp z ^ Int.negSucc a✝

Proof state:
case negSucc
z : ℂ
a✝ : ℕ
⊢ cexp (↑(Int.negSucc a✝) * z) = cexp z ^ Int.negSucc a✝

Tactic:
simp [exp_add, add_mul, pow_add, exp_neg, exp_nat_mul]

Result:
no goals

Proof state:
case ofNat
z : ℂ
a✝ : ℕ
⊢ cexp (↑(Int.ofNat a✝) * z) = cexp z ^ Int.ofNat a✝

Tactic:
simp [exp_nat_mul]

Result:
no goals
-- Mathlib/Algebra/Algebra/Quasispectrum.lean
lemma quasispectrum_eq_spectrum_union_zero (R : Type*) {A : Type*} [Semifield R] [Ring A]
    [Algebra R A] (a : A) : quasispectrum R a = spectrum R a ∪ {0}

Proof state:
R : Type u_3
A : Type u_4
inst✝² : Semifield R
inst✝¹ : Ring A
inst✝ : Algebra R A
a : A
⊢ quasispectrum R a = spectrum R a ∪ {0}

Tactic:
convert quasispectrum_eq_spectrum_union R a

Result:
case h.e'_3.h.e'_4
R : Type u_3
A : Type u_4
inst✝² : Semifield R
inst✝¹ : Ring A
inst✝ : Algebra R A
a : A
⊢ {0} = {r | ¬IsUnit r}

Proof state:
case h.e'_3.h.e'_4.h
R : Type u_3
A : Type u_4
inst✝² : Semifield R
inst✝¹ : Ring A
inst✝ : Algebra R A
a : A
x : R
⊢ x ∈ {0} ↔ x ∈ {r | ¬IsUnit r}

Tactic:
simp

Result:
no goals

Proof state:
case h.e'_3.h.e'_4
R : Type u_3
A : Type u_4
inst✝² : Semifield R
inst✝¹ : Ring A
inst✝ : Algebra R A
a : A
⊢ {0} = {r | ¬IsUnit r}

Tactic:
ext x

Result:
case h.e'_3.h.e'_4.h
R : Type u_3
A : Type u_4
inst✝² : Semifield R
inst✝¹ : Ring A
inst✝ : Algebra R A
a : A
x : R
⊢ x ∈ {0} ↔ x ∈ {r | ¬IsUnit r}
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem toListRev_eq (arr : Array α) : arr.toListRev = arr.toList.reverse

Proof state:
α : Type u_1
arr : Array α
⊢ arr.toListRev = arr.toList.reverse

Tactic:
rw [toListRev, ← foldl_toList, ← List.foldr_reverse, List.foldr_cons_nil]

Result:
no goals