harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/NumberTheory/KummerDedekind.lean
theorem emultiplicity_factors_map_eq_emultiplicity
    (hI : IsMaximal I) (hI' : I ≠ ⊥)
    (hx : (conductor R x).comap (algebraMap R S) ⊔ I = ⊤) (hx' : IsIntegral R x) {J : Ideal S}
    (hJ : J ∈ normalizedFactors (I.map (algebraMap R S))) :
    emultiplicity J (I.map (algebraMap R S)) =
      emultiplicity (↑(normalizedFactorsMapEquivNormalizedFactorsMinPolyMk hI hI' hx hx' ⟨J, hJ⟩))
        (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))

Proof state:
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
x : S
I : Ideal R
inst✝³ : IsDomain R
inst✝² : IsIntegrallyClosed R
inst✝¹ : IsDedekindDomain S
inst✝ : NoZeroSMulDivisors R S
hI : I.IsMaximal
hI' : I ≠ ⊥
hx : comap (algebraMap R S) (conductor R x) ⊔ I = ⊤
hx' : _root_.IsIntegral R x
J : Ideal S
hJ : J ∈ normalizedFactors (Ideal.map (algebraMap R S) I)
⊢ emultiplicity J (Ideal.map (algebraMap R S) I) =
    emultiplicity (↑((normalizedFactorsMapEquivNormalizedFactorsMinPolyMk hI hI' hx hx') ⟨J, hJ⟩))
      (Polynomial.map (Ideal.Quotient.mk I) (minpoly R x))

Tactic:
rw [normalizedFactorsMapEquivNormalizedFactorsMinPolyMk, Equiv.coe_trans, Function.comp_apply,
  emultiplicity_normalizedFactorsEquivSpanNormalizedFactors_symm_eq_emultiplicity,
  normalizedFactorsEquivOfQuotEquiv_emultiplicity_eq_emultiplicity]

Result:
no goals
-- Mathlib/Analysis/Normed/Field/Basic.lean
lemma norm_commutator_sub_one_le (ha : a ≠ 0) (hb : b ≠ 0) :
    ‖a * b * a⁻¹ * b⁻¹ - 1‖ ≤ 2 * ‖a‖⁻¹ * ‖b‖⁻¹ * ‖a - 1‖ * ‖b - 1‖

Proof state:
α : Type u_2
inst✝ : NormedDivisionRing α
a b : α
ha : a ≠ 0
hb : b ≠ 0
⊢ ‖a * b * a⁻¹ * b⁻¹ - 1‖ ≤ 2 * ‖a‖⁻¹ * ‖b‖⁻¹ * ‖a - 1‖ * ‖b - 1‖

Tactic:
simpa using norm_commutator_units_sub_one_le (.mk0 a ha) (.mk0 b hb)

Result:
no goals
-- Mathlib/MeasureTheory/Integral/IntervalIntegral.lean
theorem integral_add (hf : IntervalIntegrable f μ a b) (hg : IntervalIntegrable g μ a b) :
    ∫ x in a..b, f x + g x ∂μ = (∫ x in a..b, f x ∂μ) + ∫ x in a..b, g x ∂μ

Proof state:
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b : ℝ
f g : ℝ → E
μ : Measure ℝ
hf : IntervalIntegrable f μ a b
hg : IntervalIntegrable g μ a b
⊢ ∫ (x : ℝ) in a..b, f x + g x ∂μ = ∫ (x : ℝ) in a..b, f x ∂μ + ∫ (x : ℝ) in a..b, g x ∂μ

Tactic:
simp only [intervalIntegral_eq_integral_uIoc, integral_add hf.def' hg.def', smul_add]

Result:
no goals
-- Mathlib/RingTheory/WittVector/IsPoly.lean
theorem bind₁_zero_wittPolynomial [Fact p.Prime] (n : ℕ) :
    bind₁ (0 : ℕ → MvPolynomial ℕ R) (wittPolynomial p R n) = 0

Proof state:
p : ℕ
R : Type u
inst✝¹ : CommRing R
inst✝ : Fact (Nat.Prime p)
n : ℕ
⊢ (bind₁ 0) (wittPolynomial p R n) = 0

Tactic:
rw [← aeval_eq_bind₁, aeval_zero, constantCoeff_wittPolynomial, RingHom.map_zero]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/DotProduct.lean
theorem dotProduct_self_eq_zero [LinearOrderedRing R] {v : n → R} : dotProduct v v = 0 ↔ v = 0 :=
  (Finset.sum_eq_zero_iff_of_nonneg fun i _ => mul_self_nonneg (v i)).trans <| by
    simp [funext_iff]

Proof state:
n : Type u_2
R : Type u_4
inst✝¹ : Fintype n
inst✝ : LinearOrderedRing R
v : n → R
⊢ (∀ i ∈ Finset.univ, v i * v i = 0) ↔ v = 0

Tactic:
simp [funext_iff]

Result:
no goals
-- Mathlib/Order/Filter/Bases.lean
theorem HasBasis.hasBasis_self_subset {p : Set α → Prop} (h : l.HasBasis (fun s => s ∈ l ∧ p s) id)
    {V : Set α} (hV : V ∈ l) : l.HasBasis (fun s => s ∈ l ∧ p s ∧ s ⊆ V) id

Proof state:
α : Type u_1
l : Filter α
p : Set α → Prop
h : l.HasBasis (fun s => s ∈ l ∧ p s) id
V : Set α
hV : V ∈ l
⊢ l.HasBasis (fun s => s ∈ l ∧ p s ∧ s ⊆ V) id

Tactic:
simpa only [and_assoc] using h.restrict_subset hV

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Arithmetic.lean
theorem add_eq_right {a b : Cardinal} (hb : ℵ₀ ≤ b) (ha : a ≤ b) : a + b = b

Proof state:
a b : Cardinal.{u_1}
hb : ℵ₀ ≤ b
ha : a ≤ b
⊢ a + b = b

Tactic:
rw [add_comm, add_eq_left hb ha]

Result:
no goals
-- Mathlib/Algebra/Homology/HomologicalBicomplex.lean
@[reassoc]
lemma d_comm (K : HomologicalComplex₂ C c₁ c₂) (i₁ i₁' : I₁) (i₂ i₂' : I₂) :
    (K.d i₁ i₁').f i₂ ≫ (K.X i₁').d i₂ i₂' = (K.X i₁).d i₂ i₂' ≫ (K.d i₁ i₁').f i₂'

Proof state:
C : Type u_1
inst✝¹ : Category.{u_4, u_1} C
inst✝ : HasZeroMorphisms C
I₁ : Type u_2
I₂ : Type u_3
c₁ : ComplexShape I₁
c₂ : ComplexShape I₂
K : HomologicalComplex₂ C c₁ c₂
i₁ i₁' : I₁
i₂ i₂' : I₂
⊢ (K.d i₁ i₁').f i₂ ≫ (K.X i₁').d i₂ i₂' = (K.X i₁).d i₂ i₂' ≫ (K.d i₁ i₁').f i₂'

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/AC.lean
theorem Context.mergeIdem_head2 (h : x ≠ y) : mergeIdem (x :: y :: ys) = x :: mergeIdem (y :: ys)

Proof state:
x y : Nat
ys : List Nat
h : x ≠ y
⊢ mergeIdem (x :: y :: ys) = x :: mergeIdem (y :: ys)

Tactic:
simp [mergeIdem, mergeIdem.loop, h]

Result:
no goals
-- Mathlib/Topology/FiberBundle/Trivialization.lean
theorem preimageSingletonHomeomorph_symm_apply {b : B} (hb : b ∈ e.baseSet) (p : F) :
    (e.preimageSingletonHomeomorph hb).symm p =
      ⟨e.symm (b, p), by rw [mem_preimage, e.proj_symm_apply' hb, mem_singleton_iff]⟩ :=
  rfl

Proof state:
B : Type u_1
F : Type u_2
E : B → Type u_3
Z : Type u_4
inst✝³ : TopologicalSpace B
inst✝² : TopologicalSpace F
proj : Z → B
inst✝¹ : TopologicalSpace Z
inst✝ : TopologicalSpace (TotalSpace F E)
e : Trivialization F proj
x : Z
b : B
hb : b ∈ e.baseSet
p : F
⊢ ↑e.symm (b, p) ∈ proj ⁻¹' {b}

Tactic:
rw [mem_preimage, e.proj_symm_apply' hb, mem_singleton_iff]

Result:
no goals
-- Mathlib/Data/Num/Lemmas.lean
theorem cast_inj [LinearOrderedRing α] {m n : ZNum} : (m : α) = n ↔ m = n

Proof state:
α : Type u_1
inst✝ : LinearOrderedRing α
m n : ZNum
⊢ ↑m = ↑n ↔ m = n

Tactic:
rw [← cast_to_int m, ← cast_to_int n, Int.cast_inj (α := α), to_int_inj]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/BinaryBiproducts.lean
theorem biprod.associator_inv_natural {U V W X Y Z : C} (f : U ⟶ X) (g : V ⟶ Y) (h : W ⟶ Z) :
    biprod.map f (biprod.map g h) ≫ (biprod.associator _ _ _).inv
      = (biprod.associator _ _ _).inv ≫ biprod.map (biprod.map f g) h

Proof state:
C : Type uC
inst✝² : Category.{uC', uC} C
inst✝¹ : HasZeroMorphisms C
inst✝ : HasBinaryBiproducts C
U V W X Y Z : C
f : U ⟶ X
g : V ⟶ Y
h : W ⟶ Z
⊢ map f (map g h) ≫ (associator X Y Z).inv = (associator U V W).inv ≫ map (map f g) h

Tactic:
aesop_cat

Result:
no goals
-- Mathlib/CategoryTheory/Groupoid/Subgroupoid.lean
theorem mem_full_objs_iff {c : C} : c ∈ (full D).objs ↔ c ∈ D

Proof state:
C : Type u
inst✝ : Groupoid C
D : Set C
c : C
⊢ c ∈ (full D).objs ↔ c ∈ D

Tactic:
rw [full_objs]

Result:
no goals
-- Mathlib/LinearAlgebra/Finsupp/LinearCombination.lean
theorem Fintype.mem_span_image_iff_exists_fun {s : Set α} [Fintype s] :
    x ∈ span R (v '' s) ↔ ∃ c : s → R, ∑ i, c i • v i = x

Proof state:
α : Type u_1
M : Type u_2
R : Type u_3
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
v : α → M
x : M
s : Set α
inst✝ : Fintype ↑s
⊢ x ∈ span R (v '' s) ↔ ∃ c, ∑ i : ↑s, c i • v ↑i = x

Tactic:
rw [← mem_span_range_iff_exists_fun, image_eq_range]

Result:
no goals
-- Mathlib/AlgebraicTopology/DoldKan/SplitSimplicialObject.lean
theorem cofan_inj_πSummand_eq_id [HasZeroMorphisms C] {Δ : SimplexCategoryᵒᵖ} (A : IndexSet Δ) :
    (s.cofan Δ).inj A ≫ s.πSummand A = 𝟙 _

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
X : SimplicialObject C
s : Splitting X
inst✝ : HasZeroMorphisms C
Δ : SimplexCategoryᵒᵖ
A : IndexSet Δ
⊢ (s.cofan Δ).inj A ≫ s.πSummand A = 𝟙 (summand s.N Δ A)

Tactic:
simp [πSummand]

Result:
no goals
-- Mathlib/Data/Real/Sqrt.lean
@[simp] lemma sqrt_one : sqrt 1 = 1

Proof state:
⊢ sqrt 1 = 1

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/Calculus/TangentCone.lean
theorem uniqueDiffOn_Ici (a : ℝ) : UniqueDiffOn ℝ (Ici a) :=
  uniqueDiffOn_convex (convex_Ici a) <| by simp only [interior_Ici, nonempty_Ioi]

Proof state:
a : ℝ
⊢ (interior (Ici a)).Nonempty

Tactic:
simp only [interior_Ici, nonempty_Ioi]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem get_eq_get! [EquivBEq α] [LawfulHashable α] [Inhabited β] (h : m.WF) {a : α} {h} :
    get m a h = get! m a

Proof state:
α : Type u
inst✝⁴ : BEq α
inst✝³ : Hashable α
β : Type v
m : Raw α fun x => β
inst✝² : EquivBEq α
inst✝¹ : LawfulHashable α
inst✝ : Inhabited β
h✝ : m.WF
a : α
h : a ∈ m
⊢ get m a h = get! m a

Tactic:
simp_to_raw using Raw₀.Const.get_eq_get!

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Basic.lean
theorem mul_left_comm (n m k : Nat) : n * (m * k) = m * (n * k)

Proof state:
n m k : Nat
⊢ n * (m * k) = m * (n * k)

Tactic:
rw [← Nat.mul_assoc, Nat.mul_comm n m, Nat.mul_assoc]

Result:
no goals
-- Mathlib/Analysis/Normed/Algebra/TrivSqZeroExt.lean
theorem fst_exp (x : tsze R M) : fst (exp 𝕜 x) = exp 𝕜 x.fst

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
⊢ (exp 𝕜 x).fst = exp 𝕜 x.fst

Tactic:
rw [exp_def, fst_add, fst_inl, fst_inr, add_zero]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Eval/Defs.lean
theorem eval₂_zero : (0 : R[X]).eval₂ f x = 0

Proof state:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
f : R →+* S
x : S
⊢ eval₂ f x 0 = 0

Tactic:
simp [eval₂_eq_sum]

Result:
no goals
-- Mathlib/Data/Real/ConjExponents.lean
lemma conj_eq : q = p / (p - 1)

Proof state:
p q : ℝ≥0
h : p.IsConjExponent q
⊢ q = p / (p - 1)

Tactic:
simpa only [← coe_one, ← NNReal.coe_sub h.one_le, ← NNReal.coe_div, coe_inj] using h.coe.conj_eq

Result:
no goals
-- Mathlib/Data/Ordmap/Ordset.lean
theorem Valid'.rotateL_lemma₄ {a b : ℕ} (H3 : 2 * b ≤ 9 * a + 3) : 3 * b ≤ 16 * a + 9

Proof state:
a b : ℕ
H3 : 2 * b ≤ 9 * a + 3
⊢ 3 * b ≤ 16 * a + 9

Tactic:
omega

Result:
no goals
-- Mathlib/RingTheory/Ideal/Operations.lean
theorem span_singleton_mul_right_inj [IsDomain R] {x : R} (hx : x ≠ 0) :
    span {x} * I = span {x} * J ↔ I = J

Proof state:
R : Type u
inst✝¹ : CommSemiring R
I J : Ideal R
inst✝ : IsDomain R
x : R
hx : x ≠ 0
⊢ span {x} * I = span {x} * J ↔ I = J

Tactic:
simp only [le_antisymm_iff, span_singleton_mul_right_mono hx]

Result:
no goals
-- Mathlib/Analysis/Normed/Module/Dual.lean
theorem eq_zero_iff_forall_dual_eq_zero (x : E) : x = 0 ↔ ∀ g : Dual 𝕜 E, g x = 0 :=
  ⟨fun hx => by simp [hx], fun h => eq_zero_of_forall_dual_eq_zero 𝕜 h⟩

Proof state:
𝕜 : Type v
inst✝² : RCLike 𝕜
E : Type u
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
x : E
hx : x = 0
⊢ ∀ (g : Dual 𝕜 E), g x = 0

Tactic:
simp [hx]

Result:
no goals
-- Mathlib/Tactic/NormNum/Result.lean
theorem IsInt.to_isNat {α} [Ring α] : ∀ {a : α} {n}, IsInt a (.ofNat n) → IsNat a n
  | _, _, ⟨rfl⟩ => ⟨by simp⟩

Proof state:
α : Type u_1
inst✝ : Ring α
a✝ : ℕ
⊢ ↑(Int.ofNat a✝) = ↑a✝

Tactic:
simp

Result:
no goals
-- Mathlib/FieldTheory/IntermediateField/Adjoin/Basic.lean
theorem rank_bot' : Module.rank (⊥ : IntermediateField F E) E = Module.rank F E

Proof state:
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
⊢ Module.rank (↥⊥) E = Module.rank F E

Tactic:
rw [← rank_mul_rank F (⊥ : IntermediateField F E) E, IntermediateField.rank_bot, one_mul]

Result:
no goals
-- Mathlib/Topology/Sober.lean
theorem genericPoint_spec [QuasiSober α] [IrreducibleSpace α] :
    IsGenericPoint (genericPoint α) univ

Proof state:
α : Type u_1
inst✝² : TopologicalSpace α
inst✝¹ : QuasiSober α
inst✝ : IrreducibleSpace α
⊢ IsGenericPoint (genericPoint α) univ

Tactic:
simpa using (IrreducibleSpace.isIrreducible_univ α).isGenericPoint_genericPoint_closure

Result:
no goals
-- Mathlib/Data/Matroid/Dual.lean
theorem dual_isBase_iff' : M✶.IsBase B ↔ M.IsBase (M.E \ B) ∧ B ⊆ M.E :=
  (em (B ⊆ M.E)).elim (fun h ↦ by rw [dual_isBase_iff, and_iff_left h])
    (fun h ↦ iff_of_false (h ∘ (fun h' ↦ h'.subset_ground)) (h ∘ And.right))

Proof state:
α : Type u_1
M : Matroid α
B : Set α
h : B ⊆ M.E
⊢ M✶.IsBase B ↔ M.IsBase (M.E \ B) ∧ B ⊆ M.E

Tactic:
rw [dual_isBase_iff, and_iff_left h]

Result:
no goals
-- Mathlib/Analysis/Analytic/CPolynomial.lean
theorem HasFiniteFPowerSeriesOnBall.add (hf : HasFiniteFPowerSeriesOnBall f pf x n r)
    (hg : HasFiniteFPowerSeriesOnBall g pg x m r) :
    HasFiniteFPowerSeriesOnBall (f + g) (pf + pg) x (max n m) r :=
  ⟨hf.1.add hg.1, fun N hN ↦ by
    rw [Pi.add_apply, hf.finite _ ((le_max_left n m).trans hN),
        hg.finite _ ((le_max_right n m).trans hN), zero_add]⟩

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 g : E → F
pf pg : FormalMultilinearSeries 𝕜 E F
x : E
r : ℝ≥0∞
n m : ℕ
hf : HasFiniteFPowerSeriesOnBall f pf x n r
hg : HasFiniteFPowerSeriesOnBall g pg x m r
N : ℕ
hN : n ⊔ m ≤ N
⊢ (pf + pg) N = 0

Tactic:
rw [Pi.add_apply, hf.finite _ ((le_max_left n m).trans hN),
    hg.finite _ ((le_max_right n m).trans hN), zero_add]

Result:
no goals
-- Mathlib/FieldTheory/IsPerfectClosure.lean
theorem equiv_symm_apply (x : M) (n : ℕ) (y : K) (h : j y = x ^ p ^ n) :
    (equiv i j p).symm x = (iterateFrobeniusEquiv L p n).symm (i y)

Proof state:
K : Type u_1
L : Type u_2
M : Type u_3
inst✝⁹ : CommRing K
inst✝⁸ : CommRing L
inst✝⁷ : CommRing M
i : K →+* L
j : K →+* M
p : ℕ
inst✝⁶ : ExpChar M p
inst✝⁵ : ExpChar K p
inst✝⁴ : ExpChar L p
inst✝³ : PerfectRing L p
inst✝² : IsPerfectClosure i p
inst✝¹ : PerfectRing M p
inst✝ : IsPerfectClosure j p
x : M
n : ℕ
y : K
h : j y = x ^ p ^ n
⊢ (equiv i j p).symm x = (iterateFrobeniusEquiv L p n).symm (i y)

Tactic:
rw [equiv_symm, equiv_apply j i p _ _ _ h]

Result:
no goals
-- Mathlib/Topology/Inseparable.lean
theorem map_mk_nhds : map mk (𝓝 x) = 𝓝 (mk x)

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
x : X
⊢ Filter.map mk (𝓝 x) = 𝓝 (mk x)

Tactic:
rw [← comap_mk_nhds_mk, map_comap_of_surjective surjective_mk]

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Unoriented/Affine.lean
theorem _root_.Sbtw.angle₃₂₁_eq_pi {p₁ p₂ p₃ : P} (h : Sbtw ℝ p₁ p₂ p₃) : ∠ p₃ p₂ p₁ = π

Proof state:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
h : Sbtw ℝ p₁ p₂ p₃
⊢ ∠ p₃ p₂ p₁ = π

Tactic:
rw [← h.angle₁₂₃_eq_pi, angle_comm]

Result:
no goals
-- Mathlib/Algebra/Ring/Subring/Basic.lean
theorem map_comap_eq_self
    {f : R →+* S} {t : Subring S} (h : t ≤ f.range) : (t.comap f).map f = t

Proof state:
R : Type u
S : Type v
inst✝¹ : Ring R
inst✝ : Ring S
f : R →+* S
t : Subring S
h : t ≤ f.range
⊢ map f (comap f t) = t

Tactic:
simpa only [inf_of_le_left h] using Subring.map_comap_eq f t

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Bitblast.lean
theorem sshiftRightRec_zero_eq (x : BitVec w₁) (y : BitVec w₂) :
    sshiftRightRec x y 0 = x.sshiftRight' (y &&& twoPow w₂ 0)

Proof state:
w₁ w₂ : Nat
x : BitVec w₁
y : BitVec w₂
⊢ x.sshiftRightRec y 0 = x.sshiftRight' (y &&& twoPow w₂ 0)

Tactic:
simp only [sshiftRightRec]

Result:
no goals
-- Mathlib/GroupTheory/HNNExtension.lean
theorem t_mul_of (a : A) :
    t * (of (a : G) : HNNExtension G A B φ) = of (φ a : G) * t :=
  (Con.eq _).2 <| ConGen.Rel.of _ _ <| ⟨a, by simp⟩

Proof state:
G : Type u_1
inst✝ : Group G
A B : Subgroup G
φ : ↥A ≃* ↥B
a : ↥A
⊢ (fun x1 x2 => x1 * x2) (inr (ofAdd 1)) (inl ↑a) = inr (ofAdd 1) * inl ↑a ∧
    (fun x1 x2 => x1 * x2) (inl ↑(φ a)) (inr (ofAdd 1)) = inl ↑(φ a) * inr (ofAdd 1)

Tactic:
simp

Result:
no goals
-- Mathlib/Order/CompleteLattice/SetLike.lean
@[simp] lemma mem_iInf : x ∈ ⨅ i : I, f i ↔ ∀ i : I, x ∈ f i

Proof state:
X : Type u_1
L : CompleteSublattice (Set X)
I : Sort u_2
f : I → ↥L
x : X
⊢ x ∈ ⨅ i, f i ↔ ∀ (i : I), x ∈ f i

Tactic:
simp [← mem_subtype]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/Average.lean
theorem laverage_congr {f g : α → ℝ≥0∞} (h : f =ᵐ[μ] g) : ⨍⁻ x, f x ∂μ = ⨍⁻ x, g x ∂μ

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ : Measure α
f g : α → ℝ≥0∞
h : f =ᶠ[ae μ] g
⊢ ⨍⁻ (x : α), f x ∂μ = ⨍⁻ (x : α), g x ∂μ

Tactic:
simp only [laverage_eq, lintegral_congr_ae h]

Result:
no goals
-- Mathlib/SetTheory/Game/PGame.lean
theorem sub_zero_eq_add_zero (x : PGame) : x - 0 = x + 0 :=
  show x + -0 = x + 0 by rw [neg_zero]

Proof state:
x : PGame
⊢ x + -0 = x + 0

Tactic:
rw [neg_zero]

Result:
no goals
-- Mathlib/Data/ENNReal/Real.lean
theorem toNNReal_top_mul (a : ℝ≥0∞) : ENNReal.toNNReal (∞ * a) = 0

Proof state:
a : ℝ≥0∞
⊢ (⊤ * a).toNNReal = 0

Tactic:
simp

Result:
no goals
-- Mathlib/MeasureTheory/Function/SimpleFunc.lean
theorem const_lintegral_restrict (c : ℝ≥0∞) (s : Set α) :
    (const α c).lintegral (μ.restrict s) = c * μ s

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
c : ℝ≥0∞
s : Set α
⊢ (const α c).lintegral (μ.restrict s) = c * μ s

Tactic:
rw [const_lintegral, Measure.restrict_apply MeasurableSet.univ, univ_inter]

Result:
no goals
-- Mathlib/Logic/Equiv/PartialEquiv.lean
theorem trans_source' : (e.trans e').source = e.source ∩ e ⁻¹' (e.target ∩ e'.source)

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
e : PartialEquiv α β
e' : PartialEquiv β γ
⊢ (e.trans e').source = e.source ∩ ↑e ⁻¹' (e.target ∩ e'.source)

Tactic:
mfld_set_tac

Result:
no goals
-- Mathlib/Data/ENNReal/Order.lean
theorem pow_lt_top : a < ∞ → ∀ n : ℕ, a ^ n < ∞

Proof state:
a : ℝ≥0∞
⊢ a < ⊤ → ∀ (n : ℕ), a ^ n < ⊤

Tactic:
simpa only [lt_top_iff_ne_top] using pow_ne_top

Result:
no goals
-- Mathlib/Topology/Constructions.lean
theorem isClosedMap_inr : IsClosedMap (@inr X Y) := fun u hu ↦ by
  simpa [isClosed_sum_iff, preimage_image_eq u Sum.inr_injective]

Proof state:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
u : Set Y
hu : IsClosed u
⊢ IsClosed (inr '' u)

Tactic:
simpa [isClosed_sum_iff, preimage_image_eq u Sum.inr_injective]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Preserves/Shapes/Pullbacks.lean
theorem PreservesPullback.iso_hom_snd :
    (PreservesPullback.iso G f g).hom ≫ pullback.snd _ _ = G.map (pullback.snd f g)

Proof state:
C : Type u₁
inst✝⁴ : Category.{v₁, u₁} C
D : Type u₂
inst✝³ : Category.{v₂, u₂} D
G : C ⥤ D
X Y Z : C
f : X ⟶ Z
g : Y ⟶ Z
inst✝² : PreservesLimit (cospan f g) G
inst✝¹ : HasPullback f g
inst✝ : HasPullback (G.map f) (G.map g)
⊢ (iso G f g).hom ≫ pullback.snd (G.map f) (G.map g) = G.map (pullback.snd f g)

Tactic:
simp [PreservesPullback.iso]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/DivModLemmas.lean
theorem dvd_sub : ∀ {a b c : Int}, a ∣ b → a ∣ c → a ∣ b - c
  | _, _, _, ⟨d, rfl⟩, ⟨e, rfl⟩ => ⟨d - e, by rw [Int.mul_sub]⟩

Proof state:
a✝ d e : Int
⊢ a✝ * d - a✝ * e = a✝ * (d - e)

Tactic:
rw [Int.mul_sub]

Result:
no goals
-- Mathlib/GroupTheory/OrderOfElement.lean
theorem zpow_eq_one_iff_modEq {n : ℤ} : x ^ n = 1 ↔ n ≡ 0 [ZMOD orderOf x]

Proof state:
G : Type u_1
inst✝ : Group G
x : G
n : ℤ
⊢ x ^ n = 1 ↔ n ≡ 0 [ZMOD ↑(orderOf x)]

Tactic:
rw [Int.modEq_zero_iff_dvd, orderOf_dvd_iff_zpow_eq_one]

Result:
no goals
-- Mathlib/Algebra/Ring/Parity.lean
@[parity_simps] lemma odd_add : Odd (m + n) ↔ (Odd m ↔ Even n)

Proof state:
m n : ℕ
⊢ Odd (m + n) ↔ (Odd m ↔ Even n)

Tactic:
rw [← not_even_iff_odd, even_add, not_iff, ← not_even_iff_odd]

Result:
no goals
-- Mathlib/Data/Finset/Sum.lean
lemma card_toLeft_add_card_toRight : u.toLeft.card + u.toRight.card = u.card

Proof state:
α : Type u_1
β : Type u_2
u : Finset (α ⊕ β)
⊢ #u.toLeft + #u.toRight = #u

Tactic:
rw [← card_disjSum, toLeft_disjSum_toRight]

Result:
no goals
-- Mathlib/FieldTheory/IntermediateField/Adjoin/Defs.lean
theorem botEquiv_def (x : F) : botEquiv F E (algebraMap F (⊥ : IntermediateField F E) x) = x

Proof state:
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
x : F
⊢ (botEquiv F E) ((algebraMap F ↥⊥) x) = x

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Fin/Tuple/Finset.lean
lemma mem_piFinset_iff_last_init :
    f ∈ piFinset s ↔ f (last n) ∈ s (last n) ∧ init f ∈ piFinset (init s)

Proof state:
n : ℕ
α : Fin (n + 1) → Type u_1
f : (i : Fin (n + 1)) → α i
s : (i : Fin (n + 1)) → Finset (α i)
⊢ f ∈ piFinset s ↔ f (last n) ∈ s (last n) ∧ init f ∈ piFinset (init s)

Tactic:
simp only [Fintype.mem_piFinset, forall_fin_succ', init, and_comm]

Result:
no goals
-- Mathlib/Data/Fin/Tuple/Curry.lean
theorem curry_uncurry (f : Function.FromTypes p τ) : curry (uncurry f) = f

Proof state:
case zero
τ : Type u
p : Fin 0 → Type u
f : FromTypes p τ
⊢ curry f.uncurry = f

Tactic:
rfl

Result:
no goals
-- Mathlib/Data/Multiset/Sym.lean
theorem mem_sym2_iff {m : Multiset α} {z : Sym2 α} :
    z ∈ m.sym2 ↔ ∀ y ∈ z, y ∈ m :=
  m.inductionOn fun xs => by simp [List.mem_sym2_iff]

Proof state:
α : Type u_1
m : Multiset α
z : Sym2 α
xs : List α
⊢ z ∈ Multiset.sym2 ⟦xs⟧ ↔ ∀ y ∈ z, y ∈ ⟦xs⟧

Tactic:
simp [List.mem_sym2_iff]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Sat/CNF/Basic.lean
theorem not_mem_nil {v : α} : ¬Mem v ([] : Clause α)

Proof state:
α : Type u_1
v : α
⊢ ¬Mem v []

Tactic:
simp [Mem]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/BinaryProducts.lean
theorem prod_rightUnitor_inv_naturality [HasBinaryProducts C] (f : X ⟶ Y) :
    (prod.rightUnitor X).inv ≫ prod.map f (𝟙 _) = f ≫ (prod.rightUnitor Y).inv

Proof state:
C : Type u
inst✝² : Category.{v, u} C
X Y : C
inst✝¹ : HasTerminal C
inst✝ : HasBinaryProducts C
f : X ⟶ Y
⊢ (prod.rightUnitor X).inv ≫ prod.map f (𝟙 (⊤_ C)) = f ≫ (prod.rightUnitor Y).inv

Tactic:
rw [Iso.inv_comp_eq, ← Category.assoc, Iso.eq_comp_inv, prod.rightUnitor_hom_naturality]

Result:
no goals
-- Mathlib/Algebra/NeZero.lean
theorem not_neZero {n : R} : ¬NeZero n ↔ n = 0

Proof state:
R : Type u_1
inst✝ : Zero R
n : R
⊢ ¬NeZero n ↔ n = 0

Tactic:
simp [neZero_iff]

Result:
no goals
-- Mathlib/NumberTheory/Zsqrtd/Basic.lean
theorem norm_zero : norm (0 : ℤ√d) = 0

Proof state:
d : ℤ
⊢ norm 0 = 0

Tactic:
simp [norm]

Result:
no goals
-- Mathlib/Geometry/Manifold/MFDeriv/Basic.lean
theorem mfderivWithin_of_mem_nhds (h : s ∈ 𝓝 x) : mfderivWithin I I' f s x = mfderiv I I' f 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 : Set M
h : s ∈ 𝓝 x
⊢ mfderivWithin I I' f s x = mfderiv I I' f x

Tactic:
rw [← mfderivWithin_univ, ← univ_inter s, mfderivWithin_inter h]

Result:
no goals
-- Mathlib/Data/List/Duplicate.lean
theorem Duplicate.of_duplicate_cons {y : α} (h : x ∈+ y :: l) (hx : x ≠ y) : x ∈+ l

Proof state:
α : Type u_1
l : List α
x y : α
h : x ∈+ y :: l
hx : x ≠ y
⊢ x ∈+ l

Tactic:
simpa [duplicate_cons_iff, hx.symm] using h

Result:
no goals
-- Mathlib/Algebra/Algebra/Defs.lean
theorem _root_.smul_algebraMap {α : Type*} [Monoid α] [MulDistribMulAction α A]
    [SMulCommClass α R A] (a : α) (r : R) : a • algebraMap R A r = algebraMap R A r

Proof state:
R : Type u
A : Type w
inst✝⁵ : CommSemiring R
inst✝⁴ : Semiring A
inst✝³ : Algebra R A
α : Type u_2
inst✝² : Monoid α
inst✝¹ : MulDistribMulAction α A
inst✝ : SMulCommClass α R A
a : α
r : R
⊢ a • (algebraMap R A) r = (algebraMap R A) r

Tactic:
rw [algebraMap_eq_smul_one, smul_comm a r (1 : A), smul_one]

Result:
no goals
-- Mathlib/Data/List/Nodup.lean
theorem nodup_append {l₁ l₂ : List α} :
    Nodup (l₁ ++ l₂) ↔ Nodup l₁ ∧ Nodup l₂ ∧ Disjoint l₁ l₂

Proof state:
α : Type u
l₁ l₂ : List α
⊢ (l₁ ++ l₂).Nodup ↔ l₁.Nodup ∧ l₂.Nodup ∧ l₁.Disjoint l₂

Tactic:
simp only [Nodup, pairwise_append, disjoint_iff_ne]

Result:
no goals