harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Order/Group/Finset.lean
lemma fold_max_add [LinearOrder M] [Add M] [AddRightMono M] (s : Finset ι) (a : WithBot M)
    (f : ι → M) : s.fold max ⊥ (fun i ↦ ↑(f i) + a) = s.fold max ⊥ ((↑) ∘ f) + a

Proof state:
ι : Type u_1
M : Type u_3
inst✝² : LinearOrder M
inst✝¹ : Add M
inst✝ : AddRightMono M
s : Finset ι
a : WithBot M
f : ι → M
⊢ fold max ⊥ (fun i => ↑(f i) + a) s = fold max ⊥ (WithBot.some ∘ f) s + a

Tactic:
classical
  induction' s using Finset.induction_on with a s _ ih <;> simp [*, max_add_add_right]

Result:
no goals

Proof state:
ι : Type u_1
M : Type u_3
inst✝² : LinearOrder M
inst✝¹ : Add M
inst✝ : AddRightMono M
s : Finset ι
a : WithBot M
f : ι → M
⊢ fold max ⊥ (fun i => ↑(f i) + a) s = fold max ⊥ (WithBot.some ∘ f) s + a

Tactic:
induction' s using Finset.induction_on with a s _ ih <;> simp [*, max_add_add_right]

Result:
no goals
-- Mathlib/Algebra/MonoidAlgebra/Defs.lean
theorem mul_single_one_apply [MulOneClass G] (f : MonoidAlgebra k G) (r : k) (x : G) :
    (HMul.hMul (β := MonoidAlgebra k G) f (single 1 r)) x = f x * r :=
  f.mul_single_apply_aux fun a ha => by rw [mul_one]

Proof state:
k : Type u₁
G : Type u₂
inst✝¹ : Semiring k
inst✝ : MulOneClass G
f : MonoidAlgebra k G
r : k
x a : G
ha : a ∈ f.support
⊢ a * 1 = x ↔ a = x

Tactic:
rw [mul_one]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/IsLimit.lean
theorem coconePointUniqueUpToIso_hom_desc {r s t : Cocone F} (P : IsColimit s) (Q : IsColimit t) :
    (coconePointUniqueUpToIso P Q).hom ≫ Q.desc r = P.desc r :=
  P.uniq _ _ (by simp)

Proof state:
J : Type u₁
inst✝¹ : Category.{v₁, u₁} J
C : Type u₃
inst✝ : Category.{v₃, u₃} C
F : J ⥤ C
r s t : Cocone F
P : IsColimit s
Q : IsColimit t
⊢ ∀ (j : J), s.ι.app j ≫ (P.coconePointUniqueUpToIso Q).hom ≫ Q.desc r = r.ι.app j

Tactic:
simp

Result:
no goals
-- Mathlib/LinearAlgebra/Basis/Defs.lean
theorem equiv_symm : (b.equiv b' e).symm = b'.equiv b e.symm :=
  b'.ext' fun i => (b.equiv b' e).injective (by simp)

Proof state:
ι : Type u_1
ι' : Type u_2
R : Type u_3
M : Type u_6
M' : Type u_7
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : AddCommMonoid M'
inst✝ : Module R M'
b : Basis ι R M
b' : Basis ι' R M'
e : ι ≃ ι'
i : ι'
⊢ (b.equiv b' e) ((b.equiv b' e).symm (b' i)) = (b.equiv b' e) ((b'.equiv b e.symm) (b' i))

Tactic:
simp

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Basic.lean
theorem mk_range_inr {α : Type u} {β : Type v} : #(range (@Sum.inr α β)) = lift.{u} #β

Proof state:
α : Type u
β : Type v
⊢ #↑(range Sum.inr) = lift.{u, v} #β

Tactic:
rw [← lift_id'.{v, u} #_, (Equiv.Set.rangeInr α β).lift_cardinal_eq, lift_umax.{v, u}]

Result:
no goals
-- Mathlib/FieldTheory/Relrank.lean
theorem relfinrank_eq_one_of_le (h : B ≤ A) : relfinrank A B = 1

Proof state:
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
A B : IntermediateField F E
h : B ≤ A
⊢ A.relfinrank B = 1

Tactic:
simp [relfinrank_eq_toNat_relrank, relrank_eq_one_of_le h]

Result:
no goals
-- Mathlib/Probability/Kernel/Composition/MapComap.lean
lemma snd_map_prod_id (κ : Kernel α β) {f : β → γ} (hf : Measurable f) :
    snd (map κ (fun a ↦ (f a, a))) = κ

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
κ : Kernel α β
f : β → γ
hf : Measurable f
⊢ (κ.map fun a => (f a, a)).snd = κ

Tactic:
rw [snd_map_prod _ hf, Kernel.map_id']

Result:
no goals
-- Mathlib/RingTheory/Flat/CategoryTheory.lean
lemma rTensor_shortComplex_exact [Flat R M] (C : ShortComplex <| ModuleCat R) (hC : C.Exact) :
    C.map (tensorRight M) |>.Exact

Proof state:
R : Type u
inst✝¹ : CommRing R
M : ModuleCat R
inst✝ : Flat R ↑M
C : ShortComplex (ModuleCat R)
hC : C.Exact
⊢ (C.map (tensorRight M)).Exact

Tactic:
rw [moduleCat_exact_iff_function_exact] at hC ⊢

Result:
R : Type u
inst✝¹ : CommRing R
M : ModuleCat R
inst✝ : Flat R ↑M
C : ShortComplex (ModuleCat R)
hC : Function.Exact ⇑(ConcreteCategory.hom C.f) ⇑(ConcreteCategory.hom C.g)
⊢ Function.Exact ⇑(ConcreteCategory.hom (C.map (tensorRight M)).f) ⇑(ConcreteCategory.hom (C.map (tensorRight M)).g)

Proof state:
R : Type u
inst✝¹ : CommRing R
M : ModuleCat R
inst✝ : Flat R ↑M
C : ShortComplex (ModuleCat R)
hC : Function.Exact ⇑(ConcreteCategory.hom C.f) ⇑(ConcreteCategory.hom C.g)
⊢ Function.Exact ⇑(ConcreteCategory.hom (C.map (tensorRight M)).f) ⇑(ConcreteCategory.hom (C.map (tensorRight M)).g)

Tactic:
exact rTensor_exact M hC

Result:
no goals
-- Mathlib/AlgebraicGeometry/AffineScheme.lean
theorem isAffineOpen_opensRange {X Y : Scheme} [IsAffine X] (f : X ⟶ Y)
    [H : IsOpenImmersion f] : IsAffineOpen (Scheme.Hom.opensRange f)

Proof state:
X Y : Scheme
inst✝ : IsAffine X
f : X ⟶ Y
H : IsOpenImmersion f
⊢ IsAffineOpen (Scheme.Hom.opensRange f)

Tactic:
refine isAffine_of_isIso (IsOpenImmersion.isoOfRangeEq f (Y.ofRestrict _) ?_).inv

Result:
X Y : Scheme
inst✝ : IsAffine X
f : X ⟶ Y
H : IsOpenImmersion f
⊢ Set.range ⇑(ConcreteCategory.hom f.base) = Set.range ⇑(ConcreteCategory.hom (Y.ofRestrict ⋯).base)

Proof state:
X Y : Scheme
inst✝ : IsAffine X
f : X ⟶ Y
H : IsOpenImmersion f
⊢ Set.range ⇑(ConcreteCategory.hom f.base) = Set.range ⇑(ConcreteCategory.hom (Y.ofRestrict ⋯).base)

Tactic:
exact Subtype.range_val.symm

Result:
no goals
-- Mathlib/NumberTheory/ModularForms/EisensteinSeries/IsBoundedAtImInfty.lean
/-- The norm of the restricted sum is less than the full sum of the norms. -/
lemma norm_le_tsum_norm (N : ℕ) (a : Fin 2 → ZMod N) (k : ℤ) (hk : 3 ≤ k) (z : ℍ) :
    ‖eisensteinSeries a k z‖  ≤ ∑' (x : Fin 2 → ℤ), ‖eisSummand k x z‖

Proof state:
N : ℕ
a : Fin 2 → ZMod N
k : ℤ
hk : 3 ≤ k
z : ℍ
⊢ ‖eisensteinSeries a k z‖ ≤ ∑' (x : Fin 2 → ℤ), ‖eisSummand k x z‖

Tactic:
simp_rw [eisensteinSeries]

Result:
N : ℕ
a : Fin 2 → ZMod N
k : ℤ
hk : 3 ≤ k
z : ℍ
⊢ ‖∑' (x : ↑(gammaSet N a)), eisSummand k (↑x) z‖ ≤ ∑' (x : Fin 2 → ℤ), ‖eisSummand k x z‖

Proof state:
N : ℕ
a : Fin 2 → ZMod N
k : ℤ
hk : 3 ≤ k
z : ℍ
⊢ ‖∑' (x : ↑(gammaSet N a)), eisSummand k (↑x) z‖ ≤ ∑' (x : Fin 2 → ℤ), ‖eisSummand k x z‖

Tactic:
apply le_trans (norm_tsum_le_tsum_norm ((summable_norm_eisSummand hk z).subtype _))
  (tsum_subtype_le (fun (x : Fin 2 → ℤ) ↦ ‖(eisSummand k x z)‖) _ (fun _ ↦ norm_nonneg _)
    (summable_norm_eisSummand hk z))

Result:
no goals
-- Mathlib/Order/Interval/Set/Basic.lean
theorem Icc_diff_both : Icc a b \ {a, b} = Ioo a b

Proof state:
α : Type u_1
inst✝ : PartialOrder α
a b : α
⊢ Icc a b \ {a, b} = Ioo a b

Tactic:
rw [insert_eq, ← diff_diff, Icc_diff_left, Ioc_diff_right]

Result:
no goals
-- Mathlib/Algebra/Order/Group/Unbundled/Basic.lean
theorem mul_inv_le_mul_inv_iff' : a * b⁻¹ ≤ c * d⁻¹ ↔ a * d ≤ c * b

Proof state:
α : Type u
inst✝² : CommGroup α
inst✝¹ : LE α
inst✝ : MulLeftMono α
a b c d : α
⊢ a * b⁻¹ ≤ c * d⁻¹ ↔ a * d ≤ c * b

Tactic:
rw [mul_comm c, mul_inv_le_inv_mul_iff, mul_comm]

Result:
no goals
-- Mathlib/Computability/ContextFreeGrammar.lean
lemma Rewrites.input_output : r.Rewrites [.nonterminal r.input] r.output

Proof state:
T : Type u_1
N : Type u_2
r : ContextFreeRule T N
⊢ r.Rewrites [Symbol.nonterminal r.input] r.output

Tactic:
simpa using head []

Result:
no goals
-- Mathlib/Data/Multiset/Powerset.lean
theorem mem_powerset {s t : Multiset α} : s ∈ powerset t ↔ s ≤ t :=
  Quotient.inductionOn₂ s t <| by simp [Subperm, and_comm]

Proof state:
α : Type u_1
s t : Multiset α
⊢ ∀ (a b : List α), ⟦a⟧ ∈ powerset ⟦b⟧ ↔ ⟦a⟧ ≤ ⟦b⟧

Tactic:
simp [Subperm, and_comm]

Result:
no goals
-- Mathlib/RepresentationTheory/GroupCohomology/LowDegree.lean
theorem mem_oneCocycles_of_addMonoidHom [A.IsTrivial] (f : Additive G →+ A) :
    f ∘ Additive.ofMul ∈ oneCocycles A :=
  (mem_oneCocycles_iff _).2 fun g h => by
    simp only [Function.comp_apply, ofMul_mul, map_add,
      oneCocycles_map_mul_of_isTrivial, isTrivial_apply A.ρ g (f (Additive.ofMul h)),
      add_comm (f (Additive.ofMul g))]

Proof state:
k G : Type u
inst✝² : CommRing k
inst✝¹ : Group G
A : Rep k G
inst✝ : A.IsTrivial
f : Additive G →+ ↑A.V
g h : G
⊢ (⇑f ∘ ⇑Additive.ofMul) (g * h) = (A.ρ g) ((⇑f ∘ ⇑Additive.ofMul) h) + (⇑f ∘ ⇑Additive.ofMul) g

Tactic:
simp only [Function.comp_apply, ofMul_mul, map_add,
  oneCocycles_map_mul_of_isTrivial, isTrivial_apply A.ρ g (f (Additive.ofMul h)),
  add_comm (f (Additive.ofMul g))]

Result:
no goals
-- Mathlib/Algebra/Module/LocalizedModule/Basic.lean
@[simp]
lemma lift_iso (h : ∀ (x : S), IsUnit ((algebraMap R (Module.End R M'')) x))
    (x : LocalizedModule S M) :
    IsLocalizedModule.lift S f g h ((iso S f) x) = LocalizedModule.lift S g h x

Proof state:
R : Type u_1
inst✝⁷ : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
M'' : Type u_4
inst✝⁶ : AddCommMonoid M
inst✝⁵ : AddCommMonoid M'
inst✝⁴ : AddCommMonoid M''
inst✝³ : Module R M
inst✝² : Module R M'
inst✝¹ : Module R M''
f : M →ₗ[R] M'
g : M →ₗ[R] M''
inst✝ : IsLocalizedModule S f
h : ∀ (x : ↥S), IsUnit ((algebraMap R (Module.End R M'')) ↑x)
x : LocalizedModule S M
⊢ (lift S f g h) ((iso S f) x) = (LocalizedModule.lift S g h) x

Tactic:
simp [lift]

Result:
no goals
-- Mathlib/Computability/PartrecCode.lean
theorem eval_id (n) : eval Code.id n = Part.some n

Proof state:
n : ℕ
⊢ Code.id.eval n = Part.some n

Tactic:
simp! [Seq.seq, Code.id]

Result:
no goals
-- Mathlib/Data/Set/NAry.lean
theorem image2_left (h : t.Nonempty) : image2 (fun x _ => x) s t = s

Proof state:
α : Type u_1
β : Type u_3
s : Set α
t : Set β
h : t.Nonempty
⊢ image2 (fun x x_1 => x) s t = s

Tactic:
simp [nonempty_def.mp h, Set.ext_iff]

Result:
no goals
-- Mathlib/Data/Matrix/Basis.lean
theorem mul_left_apply_same (i : l) (j : m) (b : n) (M : Matrix m n α) :
    (stdBasisMatrix i j c * M) i b = c * M j b

Proof state:
l : Type u_1
m : Type u_2
n : Type u_3
α : Type u_5
inst✝³ : DecidableEq l
inst✝² : DecidableEq m
inst✝¹ : Fintype m
inst✝ : NonUnitalNonAssocSemiring α
c : α
i : l
j : m
b : n
M : Matrix m n α
⊢ (stdBasisMatrix i j c * M) i b = c * M j b

Tactic:
simp [mul_apply, stdBasisMatrix]

Result:
no goals
-- Mathlib/Topology/EMetricSpace/Defs.lean
theorem mem_closure_iff : x ∈ closure s ↔ ∀ ε > 0, ∃ y ∈ s, edist x y < ε :=
  (mem_closure_iff_nhds_basis nhds_basis_eball).trans <| by simp only [mem_ball, edist_comm x]

Proof state:
α : Type u
inst✝ : PseudoEMetricSpace α
x : α
s : Set α
⊢ (∀ (i : ℝ≥0∞), 0 < i → ∃ y ∈ s, y ∈ ball x i) ↔ ∀ ε > 0, ∃ y ∈ s, edist x y < ε

Tactic:
simp only [mem_ball, edist_comm x]

Result:
no goals
-- Mathlib/GroupTheory/Perm/Fin.lean
theorem cycleType_finRotate_of_le {n : ℕ} (h : 2 ≤ n) : cycleType (finRotate n) = {n}

Proof state:
n : ℕ
h : 2 ≤ n
⊢ (finRotate n).cycleType = {n}

Tactic:
obtain ⟨m, rfl⟩ := exists_add_of_le h

Result:
case intro
m : ℕ
h : 2 ≤ 2 + m
⊢ (finRotate (2 + m)).cycleType = {2 + m}

Proof state:
case intro
m : ℕ
h : 2 ≤ 2 + m
⊢ (finRotate (2 + m)).cycleType = {2 + m}

Tactic:
rw [add_comm, cycleType_finRotate]

Result:
no goals
-- Mathlib/Data/Int/Init.lean
lemma natCast_ne_zero {n : ℕ} : (n : ℤ) ≠ 0 ↔ n ≠ 0

Proof state:
n : ℕ
⊢ ↑n ≠ 0 ↔ n ≠ 0

Tactic:
omega

Result:
no goals
-- Mathlib/Data/Finset/NoncommProd.lean
theorem noncommProd_insert_of_not_mem [DecidableEq α] (s : Finset α) (a : α) (f : α → β) (comm)
    (ha : a ∉ s) :
    noncommProd (insert a s) f comm =
      f a * noncommProd s f (comm.mono fun _ => mem_insert_of_mem)

Proof state:
α : Type u_3
β : Type u_4
inst✝¹ : Monoid β
inst✝ : DecidableEq α
s : Finset α
a : α
f : α → β
comm : (↑(insert a s)).Pairwise (Commute on f)
ha : a ∉ s
⊢ (insert a s).noncommProd f comm = f a * s.noncommProd f ⋯

Tactic:
simp only [← cons_eq_insert _ _ ha, noncommProd_cons]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Option/Lemmas.lean
theorem isSome_iff_exists : isSome x ↔ ∃ a, x = some a

Proof state:
α✝ : Type u_1
x : Option α✝
⊢ x.isSome = true ↔ ∃ a, x = some a

Tactic:
cases x <;> simp [isSome]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Gcd.lean
theorem gcd_mul_right_left (m n : Nat) : gcd (n * m) n = n

Proof state:
m n : Nat
⊢ (n * m).gcd n = n

Tactic:
rw [Nat.mul_comm, gcd_mul_left_left]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Bool.lean
theorem toNat_le (c : Bool) : c.toNat ≤ 1

Proof state:
c : Bool
⊢ c.toNat ≤ 1

Tactic:
cases c <;> trivial

Result:
no goals
-- Mathlib/RingTheory/Valuation/ValExtension.lean
theorem val_map_eq_one_iff (x : R) : vA (algebraMap R A x) = 1 ↔ vR x = 1

Proof state:
R : Type u_1
A : Type u_2
ΓR : Type u_3
ΓA : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : Ring A
inst✝³ : LinearOrderedCommMonoidWithZero ΓR
inst✝² : LinearOrderedCommMonoidWithZero ΓA
inst✝¹ : Algebra R A
vR : Valuation R ΓR
vA : Valuation A ΓA
inst✝ : IsValExtension vR vA
x : R
⊢ vA ((algebraMap R A) x) = 1 ↔ vR x = 1

Tactic:
simpa only [le_antisymm_iff, _root_.map_one] using
  and_congr (val_map_le_iff vR vA x 1) (val_map_le_iff vR vA 1 x)

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Weierstrass.lean
lemma j_eq_zero_iff_of_char_two [IsReduced R] : W.j = 0 ↔ W.a₁ = 0

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

Tactic:
rw [j_eq_zero_iff_of_char_two', IsReduced.pow_eq_zero_iff (Nat.succ_ne_zero _)]

Result:
no goals
-- Mathlib/Combinatorics/Additive/DoublingConst.lean
@[to_additive (attr := simp) existing cast_subConst_mul_card]
lemma cast_divConst_mul_card (A B : Finset G) : (δₘ[A, B] * #A : 𝕜) = #(A / B)

Proof state:
G : Type u_1
inst✝³ : Group G
inst✝² : DecidableEq G
𝕜 : Type u_3
inst✝¹ : Semifield 𝕜
inst✝ : CharZero 𝕜
A B : Finset G
⊢ δₘ[A, B] * ↑(#A) = ↑(#(A / B))

Tactic:
exact divConst_mul_card _ _

Result:
no goals

Proof state:
G : Type u_1
inst✝³ : Group G
inst✝² : DecidableEq G
𝕜 : Type u_3
inst✝¹ : Semifield 𝕜
inst✝ : CharZero 𝕜
A B : Finset G
⊢ ↑δₘ[A, B] * ↑(#A) = ↑(#(A / B))

Tactic:
norm_cast

Result:
G : Type u_1
inst✝³ : Group G
inst✝² : DecidableEq G
𝕜 : Type u_3
inst✝¹ : Semifield 𝕜
inst✝ : CharZero 𝕜
A B : Finset G
⊢ δₘ[A, B] * ↑(#A) = ↑(#(A / B))
-- Mathlib/Analysis/InnerProductSpace/Adjoint.lean
theorem _root_.Submodule.adjoint_orthogonalProjection (U : Submodule 𝕜 E) [CompleteSpace U] :
    (orthogonalProjection U : E →L[𝕜] U)† = U.subtypeL

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝⁴ : RCLike 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace 𝕜 E
inst✝¹ : CompleteSpace E
U : Submodule 𝕜 E
inst✝ : CompleteSpace ↥U
⊢ adjoint (orthogonalProjection U) = U.subtypeL

Tactic:
rw [← U.adjoint_subtypeL, adjoint_adjoint]

Result:
no goals
-- Mathlib/Algebra/Order/BigOperators/Ring/Finset.lean
theorem sum_mul_self_eq_zero_iff [LinearOrderedSemiring R] [ExistsAddOfLE R] (s : Finset ι)
    (f : ι → R) : ∑ i ∈ s, f i * f i = 0 ↔ ∀ i ∈ s, f i = 0

Proof state:
ι : Type u_1
R : Type u_2
inst✝¹ : LinearOrderedSemiring R
inst✝ : ExistsAddOfLE R
s : Finset ι
f : ι → R
⊢ (∀ i ∈ s, f i * f i = 0) ↔ ∀ i ∈ s, f i = 0

Tactic:
simp

Result:
no goals

Proof state:
ι : Type u_1
R : Type u_2
inst✝¹ : LinearOrderedSemiring R
inst✝ : ExistsAddOfLE R
s : Finset ι
f : ι → R
⊢ ∑ i ∈ s, f i * f i = 0 ↔ ∀ i ∈ s, f i = 0

Tactic:
rw [sum_eq_zero_iff_of_nonneg fun _ _ ↦ mul_self_nonneg _]

Result:
ι : Type u_1
R : Type u_2
inst✝¹ : LinearOrderedSemiring R
inst✝ : ExistsAddOfLE R
s : Finset ι
f : ι → R
⊢ (∀ i ∈ s, f i * f i = 0) ↔ ∀ i ∈ s, f i = 0
-- Mathlib/Algebra/Polynomial/Degree/Operations.lean
theorem degree_mul_X : degree (p * X) = degree p + 1

Proof state:
R : Type u
inst✝¹ : Semiring R
inst✝ : Nontrivial R
p : R[X]
⊢ (p * X).degree = p.degree + 1

Tactic:
simp [monic_X.degree_mul]

Result:
no goals
-- Mathlib/Data/Nat/PartENat.lean
theorem withTopEquiv_symm_zero : withTopEquiv.symm 0 = 0

Proof state:
⊢ withTopEquiv.symm 0 = 0

Tactic:
simp

Result:
no goals
-- Mathlib/RingTheory/Polynomial/Cyclotomic/Basic.lean
theorem degree_cyclotomic_pos (n : ℕ) (R : Type*) (hpos : 0 < n) [Ring R] [Nontrivial R] :
    0 < (cyclotomic n R).degree

Proof state:
n : ℕ
R : Type u_1
hpos : 0 < n
inst✝¹ : Ring R
inst✝ : Nontrivial R
⊢ 0 < (cyclotomic n R).degree

Tactic:
rwa [degree_cyclotomic n R, Nat.cast_pos, Nat.totient_pos]

Result:
no goals
-- Mathlib/Data/Real/ENatENNReal.lean
@[norm_cast] lemma toENNReal_ne_top : (n : ℝ≥0∞) ≠ ∞ ↔ n ≠ ⊤

Proof state:
n : ℕ∞
⊢ ↑n ≠ ⊤ ↔ n ≠ ⊤

Tactic:
simp

Result:
no goals
-- Mathlib/FieldTheory/PurelyInseparable/PerfectClosure.lean
theorem isPurelyInseparable_adjoin_iff_pow_mem (q : ℕ) [hF : ExpChar F q] {S : Set E} :
    IsPurelyInseparable F (adjoin F S) ↔ ∀ x ∈ S, ∃ n : ℕ, x ^ q ^ n ∈ (algebraMap F E).range

Proof state:
F : Type u
E : Type v
inst✝² : Field F
inst✝¹ : Field E
inst✝ : Algebra F E
q : ℕ
hF : ExpChar F q
S : Set E
⊢ IsPurelyInseparable F ↥(adjoin F S) ↔ ∀ x ∈ S, ∃ n, x ^ q ^ n ∈ (algebraMap F E).range

Tactic:
simp_rw [← le_perfectClosure_iff, adjoin_le_iff, ← mem_perfectClosure_iff_pow_mem q,
  Set.subset_def, SetLike.mem_coe]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Lemmas.lean
theorem mul_assoc (a b c : Int) : a * b * c = a * (b * c)

Proof state:
a b c : Int
⊢ a * b * c = a * (b * c)

Tactic:
cases a <;> cases b <;> cases c <;> simp [Nat.mul_assoc]

Result:
no goals
-- Mathlib/RingTheory/Ideal/Operations.lean
theorem isCoprime_iff_add : IsCoprime I J ↔ I + J = 1

Proof state:
R : Type u
inst✝ : CommSemiring R
I J : Ideal R
⊢ IsCoprime I J ↔ I + J = 1

Tactic:
rw [isCoprime_iff_codisjoint, codisjoint_iff, add_eq_sup, one_eq_top]

Result:
no goals
-- Mathlib/Algebra/GroupWithZero/Associated.lean
theorem decompositionMonoid_iff : DecompositionMonoid (Associates M) ↔ DecompositionMonoid M

Proof state:
M : Type u_1
inst✝ : CommMonoid M
⊢ DecompositionMonoid (Associates M) ↔ DecompositionMonoid M

Tactic:
simp_rw [_root_.decompositionMonoid_iff, forall_associated, isPrimal_mk]

Result:
no goals
-- Mathlib/CategoryTheory/Abelian/Projective/Resolution.lean
theorem homotopyEquiv_hom_π {X : C} (P Q : ProjectiveResolution X) :
    (homotopyEquiv P Q).hom ≫ Q.π = P.π

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Abelian C
X : C
P Q : ProjectiveResolution X
⊢ (P.homotopyEquiv Q).hom ≫ Q.π = P.π

Tactic:
simp [homotopyEquiv]

Result:
no goals
-- Mathlib/Data/Int/GCD.lean
theorem gcd_div_gcd_div_gcd {i j : ℤ} (H : 0 < gcd i j) : gcd (i / gcd i j) (j / gcd i j) = 1

Proof state:
i j : ℤ
H : 0 < i.gcd j
⊢ (i / ↑(i.gcd j)).gcd (j / ↑(i.gcd j)) = 1

Tactic:
rw [gcd_div gcd_dvd_left gcd_dvd_right, natAbs_ofNat, Nat.div_self H]

Result:
no goals
-- Mathlib/Combinatorics/Colex.lean
private lemma max_mem_aux {s t : Colex α} (hst : s ≠ t) : (ofColex s ∆ ofColex t).Nonempty

Proof state:
α : Type u_1
inst✝ : LinearOrder α
s t : Colex α
hst : s ≠ t
⊢ (s.ofColex ∆ t.ofColex).Nonempty

Tactic:
simpa

Result:
no goals
-- Mathlib/LinearAlgebra/TensorProduct/RightExactness.lean
/-- Right-exactness of tensor product (`rTensor`) -/
lemma rTensor_mkQ (N : Submodule R M) :
    ker (rTensor Q (N.mkQ)) = range (rTensor Q N.subtype)

Proof state:
R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
Q : Type u_5
inst✝¹ : AddCommGroup Q
inst✝ : Module R Q
N : Submodule R M
⊢ Exact ⇑(rTensor Q N.subtype) ⇑(rTensor Q N.mkQ)

Tactic:
exact rTensor_exact Q (LinearMap.exact_subtype_mkQ N) (Submodule.mkQ_surjective N)

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
Q : Type u_5
inst✝¹ : AddCommGroup Q
inst✝ : Module R Q
N : Submodule R M
⊢ ker (rTensor Q N.mkQ) = range (rTensor Q N.subtype)

Tactic:
rw [← exact_iff]

Result:
R : Type u_1
M : Type u_2
inst✝⁴ : CommRing R
inst✝³ : AddCommGroup M
inst✝² : Module R M
Q : Type u_5
inst✝¹ : AddCommGroup Q
inst✝ : Module R Q
N : Submodule R M
⊢ Exact ⇑(rTensor Q N.subtype) ⇑(rTensor Q N.mkQ)
-- Mathlib/Analysis/SpecialFunctions/Pow/Real.lean
lemma rpow_sub_intCast' (hx : 0 ≤ x) {n : ℤ} (h : y - n ≠ 0) : x ^ (y - n) = x ^ y / x ^ n

Proof state:
x y : ℝ
hx : 0 ≤ x
n : ℤ
h : y - ↑n ≠ 0
⊢ x ^ (y - ↑n) = x ^ y / x ^ n

Tactic:
rw [rpow_sub' hx h, rpow_intCast]

Result:
no goals
-- Mathlib/Data/ENNReal/Basic.lean
theorem ofReal_toReal {a : ℝ≥0∞} (h : a ≠ ∞) : ENNReal.ofReal a.toReal = a

Proof state:
a : ℝ≥0∞
h : a ≠ ⊤
⊢ ENNReal.ofReal a.toReal = a

Tactic:
simp [ENNReal.toReal, ENNReal.ofReal, h]

Result:
no goals
-- Mathlib/RingTheory/FiniteType.lean
theorem of_surjective (f : A →+* B) (hf : Surjective f) : f.FiniteType

Proof state:
A : Type u_1
B : Type u_2
inst✝¹ : CommRing A
inst✝ : CommRing B
f : A →+* B
hf : Surjective ⇑f
⊢ f.FiniteType

Tactic:
rw [← f.comp_id]

Result:
A : Type u_1
B : Type u_2
inst✝¹ : CommRing A
inst✝ : CommRing B
f : A →+* B
hf : Surjective ⇑f
⊢ (f.comp (RingHom.id A)).FiniteType

Proof state:
A : Type u_1
B : Type u_2
inst✝¹ : CommRing A
inst✝ : CommRing B
f : A →+* B
hf : Surjective ⇑f
⊢ (f.comp (RingHom.id A)).FiniteType

Tactic:
exact (id A).comp_surjective hf

Result:
no goals
-- Mathlib/Probability/CDF.lean
@[simp] lemma MeasureTheory.Measure.cdf_eq_iff (μ ν : Measure ℝ) [IsProbabilityMeasure μ]
    [IsProbabilityMeasure ν] :
    cdf μ = cdf ν ↔ μ = ν :=
⟨MeasureTheory.Measure.eq_of_cdf μ ν, fun h ↦ by rw [h]⟩

Proof state:
μ ν : Measure ℝ
inst✝¹ : IsProbabilityMeasure μ
inst✝ : IsProbabilityMeasure ν
h : μ = ν
⊢ cdf μ = cdf ν

Tactic:
rw [h]

Result:
no goals
-- Mathlib/Data/Matrix/Mul.lean
theorem mulVec_single_one [Fintype n] [DecidableEq n] [NonAssocSemiring R]
    (M : Matrix m n R) (j : n) :
    M *ᵥ Pi.single j 1 = Mᵀ j

Proof state:
case h
m : Type u_2
n : Type u_3
R : Type u_7
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : NonAssocSemiring R
M : Matrix m n R
j : n
x✝ : m
⊢ (M *ᵥ Pi.single j 1) x✝ = Mᵀ j x✝

Tactic:
simp

Result:
no goals

Proof state:
m : Type u_2
n : Type u_3
R : Type u_7
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : NonAssocSemiring R
M : Matrix m n R
j : n
⊢ M *ᵥ Pi.single j 1 = Mᵀ j

Tactic:
ext

Result:
case h
m : Type u_2
n : Type u_3
R : Type u_7
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : NonAssocSemiring R
M : Matrix m n R
j : n
x✝ : m
⊢ (M *ᵥ Pi.single j 1) x✝ = Mᵀ j x✝
-- Mathlib/.lake/packages/lean4/src/lean/Std/Tactic/BVDecide/LRAT/Internal/Formula/RupAddResult.lean
theorem rupUnits_performRupCheck {n : Nat} (f : DefaultFormula n) (rupHints : Array Nat) :
    (performRupCheck f rupHints).1.rupUnits = f.rupUnits

Proof state:
n : Nat
f : DefaultFormula n
rupHints : Array Nat
⊢ (f.performRupCheck rupHints).fst.rupUnits = f.rupUnits

Tactic:
simp only [performRupCheck]

Result:
no goals
-- Mathlib/Data/Complex/Trigonometric.lean
theorem sinh_sub_cosh : sinh x - cosh x = -exp (-x)

Proof state:
x : ℂ
⊢ sinh x - cosh x = -cexp (-x)

Tactic:
rw [← neg_sub, cosh_sub_sinh]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Laurent.lean
theorem T_sub (m n : ℤ) : (T (m - n) : R[T;T⁻¹]) = T m * T (-n)

Proof state:
R : Type u_1
inst✝ : Semiring R
m n : ℤ
⊢ T (m - n) = T m * T (-n)

Tactic:
rw [← T_add, sub_eq_add_neg]

Result:
no goals
-- Mathlib/Data/Matrix/Notation.lean
theorem submatrix_cons_row (A : Matrix m' n' α) (i : m') (row : Fin m → m') (col : o' → n') :
    submatrix A (vecCons i row) col = vecCons (fun j => A i (col j)) (submatrix A row col)

Proof state:
case a
α : Type u
m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
A : Matrix m' n' α
i✝ : m'
row : Fin m → m'
col : o' → n'
i : Fin m.succ
j : o'
⊢ A.submatrix (vecCons i✝ row) col i j = vecCons (fun j => A i✝ (col j)) (A.submatrix row col) i j

Tactic:
refine Fin.cases ?_ ?_ i <;> simp [submatrix]

Result:
no goals

Proof state:
α : Type u
m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
A : Matrix m' n' α
i : m'
row : Fin m → m'
col : o' → n'
⊢ A.submatrix (vecCons i row) col = vecCons (fun j => A i (col j)) (A.submatrix row col)

Tactic:
ext i j

Result:
case a
α : Type u
m : ℕ
m' : Type uₘ
n' : Type uₙ
o' : Type uₒ
A : Matrix m' n' α
i✝ : m'
row : Fin m → m'
col : o' → n'
i : Fin m.succ
j : o'
⊢ A.submatrix (vecCons i✝ row) col i j = vecCons (fun j => A i✝ (col j)) (A.submatrix row col) i j
-- Mathlib/Topology/Instances/EReal/Lemmas.lean
theorem nhds_bot : 𝓝 (⊥ : EReal) = ⨅ (a) (_ : a ≠ ⊥), 𝓟 (Iio a) :=
  nhds_bot_order.trans <| by simp only [bot_lt_iff_ne_bot]

Proof state:
⊢ ⨅ l, ⨅ (_ : ⊥ < l), 𝓟 (Iio l) = ⨅ a, ⨅ (_ : a ≠ ⊥), 𝓟 (Iio a)

Tactic:
simp only [bot_lt_iff_ne_bot]

Result:
no goals