harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/BigOperators/Group/Finset/Basic.lean
theorem prod_unique_nonempty {α β : Type*} [CommMonoid β] [Unique α] (s : Finset α) (f : α → β)
    (h : s.Nonempty) : ∏ x ∈ s, f x = f default

Proof state:
α : Type u_6
β : Type u_7
inst✝¹ : CommMonoid β
inst✝ : Unique α
s : Finset α
f : α → β
h : s.Nonempty
⊢ ∏ x ∈ s, f x = f default

Tactic:
rw [h.eq_singleton_default, Finset.prod_singleton]

Result:
no goals
-- Mathlib/Algebra/GCDMonoid/Finset.lean
theorem gcd_congr {f g : β → α} (hs : s₁ = s₂) (hfg : ∀ a ∈ s₂, f a = g a) :
    s₁.gcd f = s₂.gcd g

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s₁ : Finset β
f g : β → α
hfg : ∀ a ∈ s₁, f a = g a
⊢ s₁.gcd f = s₁.gcd g

Tactic:
exact Finset.fold_congr hfg

Result:
no goals

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s₁ s₂ : Finset β
f g : β → α
hs : s₁ = s₂
hfg : ∀ a ∈ s₂, f a = g a
⊢ s₁.gcd f = s₂.gcd g

Tactic:
subst hs

Result:
α : Type u_2
β : Type u_3
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s₁ : Finset β
f g : β → α
hfg : ∀ a ∈ s₁, f a = g a
⊢ s₁.gcd f = s₁.gcd g
-- Mathlib/Geometry/Euclidean/Angle/Unoriented/RightAngle.lean
theorem dist_sq_eq_dist_sq_add_dist_sq_iff_angle_eq_pi_div_two (p₁ p₂ p₃ : P) :
    dist p₁ p₃ * dist p₁ p₃ = dist p₁ p₂ * dist p₁ p₂ + dist p₃ p₂ * dist p₃ p₂ ↔
      ∠ p₁ p₂ p₃ = π / 2

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
⊢ dist p₁ p₃ * dist p₁ p₃ = dist p₁ p₂ * dist p₁ p₂ + dist p₃ p₂ * dist p₃ p₂ ↔ ∠ p₁ p₂ p₃ = π / 2

Tactic:
erw [dist_comm p₃ p₂, dist_eq_norm_vsub V p₁ p₃, dist_eq_norm_vsub V p₁ p₂,
  dist_eq_norm_vsub V p₂ p₃, ← norm_sub_sq_eq_norm_sq_add_norm_sq_iff_angle_eq_pi_div_two,
  vsub_sub_vsub_cancel_right p₁, ← neg_vsub_eq_vsub_rev p₂ p₃, norm_neg]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem replicate_eq_append_iff {l₁ l₂ : List α} {a : α} :
    replicate n a = l₁ ++ l₂ ↔
      l₁.length + l₂.length = n ∧ l₁ = replicate l₁.length a ∧ l₂ = replicate l₂.length a

Proof state:
α : Type u_1
n : Nat
l₁ l₂ : List α
a : α
⊢ replicate n a = l₁ ++ l₂ ↔ l₁.length + l₂.length = n ∧ l₁ = replicate l₁.length a ∧ l₂ = replicate l₂.length a

Tactic:
rw [eq_comm, append_eq_replicate_iff]

Result:
no goals
-- Mathlib/Analysis/Calculus/DSlope.lean
theorem dslope_same (f : 𝕜 → E) (a : 𝕜) : dslope f a a = deriv f a

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
a : 𝕜
⊢ dslope f a a = deriv f a

Tactic:
exact update_self ..

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : NontriviallyNormedField 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace 𝕜 E
f : 𝕜 → E
a : 𝕜
⊢ dslope f a a = deriv f a

Tactic:
classical
exact update_self ..

Result:
no goals
-- Mathlib/Order/BooleanSubalgebra.lean
lemma map_inf (L M : BooleanSubalgebra α) (f : BoundedLatticeHom α β) (hf : Injective f) :
    map f (L ⊓ M) = map f L ⊓ map f M

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : BooleanAlgebra α
inst✝ : BooleanAlgebra β
L M : BooleanSubalgebra α
f : BoundedLatticeHom α β
hf : Injective ⇑f
⊢ map f (L ⊓ M) = map f L ⊓ map f M

Tactic:
rw [← SetLike.coe_set_eq]

Result:
α : Type u_2
β : Type u_3
inst✝¹ : BooleanAlgebra α
inst✝ : BooleanAlgebra β
L M : BooleanSubalgebra α
f : BoundedLatticeHom α β
hf : Injective ⇑f
⊢ ↑(map f (L ⊓ M)) = ↑(map f L ⊓ map f M)

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : BooleanAlgebra α
inst✝ : BooleanAlgebra β
L M : BooleanSubalgebra α
f : BoundedLatticeHom α β
hf : Injective ⇑f
⊢ ↑(map f (L ⊓ M)) = ↑(map f L ⊓ map f M)

Tactic:
simp [Set.image_inter hf]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Order.lean
theorem ofNat_lt {n m : Nat} : (↑n : Int) < ↑m ↔ n < m

Proof state:
n m : Nat
⊢ ↑n < ↑m ↔ n < m

Tactic:
rw [lt_iff_add_one_le, ← ofNat_succ, ofNat_le]

Result:
n m : Nat
⊢ n.succ ≤ m ↔ n < m

Proof state:
n m : Nat
⊢ n.succ ≤ m ↔ n < m

Tactic:
rfl

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Bitwise/Lemmas.lean
theorem shiftRight_bitwise_distrib {a b : Nat} (of_false_false : f false false = false

Proof state:
f : Bool → Bool → Bool
i a b : Nat
of_false_false : autoParam (f false false = false) _auto✝
⊢ bitwise f a b >>> i = bitwise f (a >>> i) (b >>> i)

Tactic:
simp [shiftRight_eq_div_pow, bitwise_div_two_pow of_false_false]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/Lebesgue.lean
theorem lintegral_eq_top_of_measure_eq_top_ne_zero {f : α → ℝ≥0∞} (hf : AEMeasurable f μ)
    (hμf : μ {x | f x = ∞} ≠ 0) : ∫⁻ x, f x ∂μ = ∞ :=
  eq_top_iff.mpr <|
    calc
      ∞ = ∞ * μ { x | ∞ ≤ f x }

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
hμf : μ {x | f x = ⊤} ≠ 0
⊢ ⊤ = ⊤ * μ {x | ⊤ ≤ f x}

Tactic:
simp [mul_eq_top, hμf]

Result:
no goals
-- Mathlib/Order/Interval/Finset/Basic.lean
theorem Ioc_union_Ioc_eq_Ioc {a b c : α} (h₁ : a ≤ b) (h₂ : b ≤ c) :
    Ioc a b ∪ Ioc b c = Ioc a c

Proof state:
α : Type u_2
inst✝¹ : LinearOrder α
inst✝ : LocallyFiniteOrder α
a b c : α
h₁ : a ≤ b
h₂ : b ≤ c
⊢ Ioc a b ∪ Ioc b c = Ioc a c

Tactic:
rw [← coe_inj, coe_union, coe_Ioc, coe_Ioc, coe_Ioc, Set.Ioc_union_Ioc_eq_Ioc h₁ h₂]

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

Proof state:
⊢ ∀ {a b : Bool}, (a = false ↔ b = false) ↔ (!a) = !b

Tactic:
decide

Result:
no goals
-- Mathlib/RingTheory/Spectrum/Prime/Topology.lean
theorem basicOpen_le_basicOpen_iff (f g : R) :
    basicOpen f ≤ basicOpen g ↔ f ∈ (Ideal.span ({g} : Set R)).radical

Proof state:
R : Type u
inst✝ : CommSemiring R
f g : R
⊢ basicOpen f ≤ basicOpen g ↔ f ∈ (Ideal.span {g}).radical

Tactic:
rw [← SetLike.coe_subset_coe, basicOpen_eq_zeroLocus_compl, basicOpen_eq_zeroLocus_compl,
  Set.compl_subset_compl, zeroLocus_subset_zeroLocus_singleton_iff]

Result:
no goals
-- Mathlib/NumberTheory/PellMatiyasevic.lean
theorem y_mul_dvd (n) : ∀ k, yn a1 n ∣ yn a1 (n * k)
  | 0 => dvd_zero _
  | k + 1 => by
    rw [Nat.mul_succ, yn_add]; exact dvd_add (dvd_mul_left _ _) ((y_mul_dvd _ k).mul_right _)

Proof state:
a : ℕ
a1 : 1 < a
n k : ℕ
⊢ yn a1 n ∣ yn a1 (n * (k + 1))

Tactic:
rw [Nat.mul_succ, yn_add]

Result:
a : ℕ
a1 : 1 < a
n k : ℕ
⊢ yn a1 n ∣ xn a1 (n * k) * yn a1 n + yn a1 (n * k) * xn a1 n

Proof state:
a : ℕ
a1 : 1 < a
n k : ℕ
⊢ yn a1 n ∣ xn a1 (n * k) * yn a1 n + yn a1 (n * k) * xn a1 n

Tactic:
exact dvd_add (dvd_mul_left _ _) ((y_mul_dvd _ k).mul_right _)

Result:
no goals
-- Mathlib/RingTheory/Ideal/Maps.lean
theorem Module.annihilator_eq_top_iff : annihilator R M = ⊤ ↔ Subsingleton M :=
  ⟨fun h ↦ ⟨fun m m' ↦ by
      rw [← one_smul R m, ← one_smul R m']
      simp_rw [mem_annihilator.mp (h ▸ Submodule.mem_top)]⟩,
    fun _ ↦ top_le_iff.mp fun _ _ ↦ mem_annihilator.mpr fun _ ↦ Subsingleton.elim _ _⟩

Proof state:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
h : annihilator R M = ⊤
m m' : M
⊢ 1 • m = 1 • m'

Tactic:
simp_rw [mem_annihilator.mp (h ▸ Submodule.mem_top)]

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
h : annihilator R M = ⊤
m m' : M
⊢ m = m'

Tactic:
rw [← one_smul R m, ← one_smul R m']

Result:
R : Type u_1
M : Type u_2
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
h : annihilator R M = ⊤
m m' : M
⊢ 1 • m = 1 • m'
-- Mathlib/Algebra/Module/ZLattice/Covolume.lean
theorem volume_image_eq_volume_div_covolume {ι : Type*} [Fintype ι] [DecidableEq ι]
    (L : Submodule ℤ (ι → ℝ)) [DiscreteTopology L] [IsZLattice ℝ L] (b : Basis ι ℤ L)
    {s : Set (ι → ℝ)} :
    volume ((b.ofZLatticeBasis ℝ L).equivFun '' s) = volume s / ENNReal.ofReal (covolume L)

Proof state:
ι : Type u_2
inst✝³ : Fintype ι
inst✝² : DecidableEq ι
L : Submodule ℤ (ι → ℝ)
inst✝¹ : DiscreteTopology ↥L
inst✝ : IsZLattice ℝ L
b : Basis ι ℤ ↥L
s : Set (ι → ℝ)
⊢ volume (⇑(Basis.ofZLatticeBasis ℝ L b).equivFun '' s) = volume s / ENNReal.ofReal (covolume L volume)

Tactic:
rw [LinearEquiv.image_eq_preimage, Measure.addHaar_preimage_linearEquiv, LinearEquiv.symm_symm,
  covolume_eq_det_inv L b, ENNReal.div_eq_inv_mul, ENNReal.ofReal_inv_of_pos
  (abs_pos.mpr (LinearEquiv.det _).ne_zero), inv_inv, LinearEquiv.coe_det]

Result:
no goals
-- Mathlib/Algebra/BigOperators/Fin.lean
theorem partialProd_right_inv {G : Type*} [Group G] (f : Fin n → G) (i : Fin n) :
    (partialProd f (Fin.castSucc i))⁻¹ * partialProd f i.succ = f i

Proof state:
n : ℕ
G : Type u_3
inst✝ : Group G
f : Fin n → G
i : Fin n
⊢ (partialProd f i.castSucc)⁻¹ * partialProd f i.succ = f i

Tactic:
rw [partialProd_succ, inv_mul_cancel_left]

Result:
no goals
-- Mathlib/Algebra/Ring/Equiv.lean
theorem piCongrLeft'_symm {R : Type*} [NonUnitalNonAssocSemiring R] (e : α ≃ β) :
    (RingEquiv.piCongrLeft' (fun _ => R) e).symm = RingEquiv.piCongrLeft' _ e.symm

Proof state:
α : Type u_2
β : Type u_3
R : Type u_7
inst✝ : NonUnitalNonAssocSemiring R
e : α ≃ β
⊢ (piCongrLeft' (fun x => R) e).symm = piCongrLeft' (fun i => R) e.symm

Tactic:
simp only [piCongrLeft', RingEquiv.symm, MulEquiv.symm, Equiv.piCongrLeft'_symm]

Result:
no goals
-- Mathlib/Order/Lattice.lean
theorem SemilatticeInf.ext_inf {α} {A B : SemilatticeInf α}
    (H : ∀ x y : α, (haveI := A; x ≤ y) ↔ x ≤ y)
    (x y : α) :
    (haveI := A; x ⊓ y) = x ⊓ y :=
  eq_of_forall_le_iff fun c => by simp only [le_inf_iff]; rw [← H, @le_inf_iff α A, H, H]

Proof state:
α : Type u_1
A B : SemilatticeInf α
H : ∀ (x y : α), x ≤ y ↔ x ≤ y
x y c : α
⊢ c ≤ x ⊓ y ↔ c ≤ x ⊓ y

Tactic:
simp only [le_inf_iff]

Result:
α : Type u_1
A B : SemilatticeInf α
H : ∀ (x y : α), x ≤ y ↔ x ≤ y
x y c : α
⊢ c ≤ x ⊓ y ↔ c ≤ x ∧ c ≤ y

Proof state:
α : Type u_1
A B : SemilatticeInf α
H : ∀ (x y : α), x ≤ y ↔ x ≤ y
x y c : α
⊢ c ≤ x ⊓ y ↔ c ≤ x ∧ c ≤ y

Tactic:
rw [← H, @le_inf_iff α A, H, H]

Result:
no goals
-- Mathlib/Data/Fin/Basic.lean
lemma predAbove_castPred_of_le (p i : Fin (n + 1)) (h : i ≤ p) (hp : p ≠ last n)
    (hi := Fin.ne_of_lt <| Fin.lt_of_le_of_lt h <| Fin.lt_last_iff_ne_last.2 hp) :
    (castPred p hp).predAbove i = castPred i hi

Proof state:
n : ℕ
p i : Fin (n + 1)
h : i ≤ p
hp : p ≠ last n
hi : optParam (i ≠ last n) ⋯
⊢ (p.castPred hp).predAbove i = i.castPred hi

Tactic:
rw [predAbove_of_le_castSucc _ _ (castSucc_castPred _ _ ▸ h)]

Result:
no goals
-- Mathlib/RingTheory/PowerSeries/Order.lean
theorem order_X : order (X : R⟦X⟧) = 1

Proof state:
R : Type u_1
inst✝¹ : Semiring R
inst✝ : Nontrivial R
⊢ X.order = 1

Tactic:
simpa only [Nat.cast_one] using order_monomial_of_ne_zero 1 (1 : R) one_ne_zero

Result:
no goals
-- Mathlib/Data/Holor.lean
theorem take_take : ∀ t : HolorIndex (ds₁ ++ ds₂ ++ ds₃), t.assocRight.take = t.take.take
  | ⟨is, h⟩ =>
    Subtype.eq <| by
      simp [assocRight, take, cast_type, List.take_take, Nat.le_add_right, min_eq_left]

Proof state:
ds₁ ds₂ ds₃ is : List ℕ
h : Forall₂ (fun x1 x2 => x1 < x2) is (ds₁ ++ ds₂ ++ ds₃)
⊢ ↑(assocRight ⟨is, h⟩).take = ↑(take ⟨is, h⟩).take

Tactic:
simp [assocRight, take, cast_type, List.take_take, Nat.le_add_right, min_eq_left]

Result:
no goals
-- Mathlib/Topology/UniformSpace/UniformConvergenceTopology.lean
theorem iInf_eq {u : ι → UniformSpace γ} :
    𝒱(α, γ, 𝔖, ⨅ i, u i) = ⨅ i, 𝒱(α, γ, 𝔖, u i)

Proof state:
α : Type u_1
γ : Type u_3
ι : Type u_4
𝔖 : Set (Set α)
u : ι → UniformSpace γ
⊢ ⨅ s ∈ 𝔖, ⨅ i, UniformSpace.comap (⇑UniformFun.ofFun ∘ s.restrict ∘ ⇑(toFun 𝔖)) (UniformFun.uniformSpace (↑s) γ) =
    ⨅ i, ⨅ s ∈ 𝔖, UniformSpace.comap (⇑UniformFun.ofFun ∘ s.restrict ∘ ⇑(toFun 𝔖)) (UniformFun.uniformSpace (↑s) γ)

Tactic:
rw [iInf_comm]

Result:
α : Type u_1
γ : Type u_3
ι : Type u_4
𝔖 : Set (Set α)
u : ι → UniformSpace γ
⊢ ⨅ s ∈ 𝔖, ⨅ i, UniformSpace.comap (⇑UniformFun.ofFun ∘ s.restrict ∘ ⇑(toFun 𝔖)) (UniformFun.uniformSpace (↑s) γ) =
    ⨅ j,
      ⨅ i,
        ⨅ (_ : j ∈ 𝔖), UniformSpace.comap (⇑UniformFun.ofFun ∘ j.restrict ∘ ⇑(toFun 𝔖)) (UniformFun.uniformSpace (↑j) γ)

Proof state:
α : Type u_1
γ : Type u_3
ι : Type u_4
𝔖 : Set (Set α)
u : ι → UniformSpace γ
⊢ uniformSpace α γ 𝔖 = ⨅ i, uniformSpace α γ 𝔖

Tactic:
simp_rw [UniformOnFun.uniformSpace, UniformFun.iInf_eq, UniformSpace.comap_iInf]

Result:
α : Type u_1
γ : Type u_3
ι : Type u_4
𝔖 : Set (Set α)
u : ι → UniformSpace γ
⊢ ⨅ s ∈ 𝔖, ⨅ i, UniformSpace.comap (⇑UniformFun.ofFun ∘ s.restrict ∘ ⇑(toFun 𝔖)) (UniformFun.uniformSpace (↑s) γ) =
    ⨅ i, ⨅ s ∈ 𝔖, UniformSpace.comap (⇑UniformFun.ofFun ∘ s.restrict ∘ ⇑(toFun 𝔖)) (UniformFun.uniformSpace (↑s) γ)

Proof state:
α : Type u_1
γ : Type u_3
ι : Type u_4
𝔖 : Set (Set α)
u : ι → UniformSpace γ
⊢ ⨅ s ∈ 𝔖, ⨅ i, UniformSpace.comap (⇑UniformFun.ofFun ∘ s.restrict ∘ ⇑(toFun 𝔖)) (UniformFun.uniformSpace (↑s) γ) =
    ⨅ j,
      ⨅ i,
        ⨅ (_ : j ∈ 𝔖), UniformSpace.comap (⇑UniformFun.ofFun ∘ j.restrict ∘ ⇑(toFun 𝔖)) (UniformFun.uniformSpace (↑j) γ)

Tactic:
exact iInf_congr fun s => iInf_comm

Result:
no goals
-- Mathlib/Topology/DerivedSet.lean
lemma perfect_iff_eq_derivedSet {U : Set X} : Perfect U ↔ U = derivedSet U

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
U : Set X
⊢ Perfect U ↔ U = derivedSet U

Tactic:
rw [perfect_def, isClosed_iff_derivedSet_subset, preperfect_iff_subset_derivedSet,
  ← subset_antisymm_iff, eq_comm]

Result:
no goals
-- Mathlib/GroupTheory/Coset/Defs.lean
theorem mk_out_eq_mul (g : α) : ∃ h : s, (mk g : α ⧸ s).out = g * h :=
  ⟨⟨g⁻¹ * (mk g).out, QuotientGroup.eq.mp (mk g).out_eq'.symm⟩, by rw [mul_inv_cancel_left]⟩

Proof state:
α : Type u_1
inst✝ : Group α
s : Subgroup α
g : α
⊢ Quotient.out ↑g = g * ↑⟨g⁻¹ * Quotient.out ↑g, ⋯⟩

Tactic:
rw [mul_inv_cancel_left]

Result:
no goals
-- Mathlib/Algebra/MonoidAlgebra/ToDirectSum.lean
theorem DirectSum.toAddMonoidAlgebra_pow [DecidableEq ι] [AddMonoid ι] [Semiring M]
    [∀ m : M, Decidable (m ≠ 0)] (f : ⨁ _ : ι, M) (n : ℕ):
    (f ^ n).toAddMonoidAlgebra = toAddMonoidAlgebra f ^ n :=  by
  classical exact map_pow addMonoidAlgebraRingEquivDirectSum.symm f n

Proof state:
ι : Type u_1
M : Type u_3
inst✝³ : DecidableEq ι
inst✝² : AddMonoid ι
inst✝¹ : Semiring M
inst✝ : (m : M) → Decidable (m ≠ 0)
f : ⨁ (x : ι), M
n : ℕ
⊢ (f ^ n).toAddMonoidAlgebra = f.toAddMonoidAlgebra ^ n

Tactic:
classical exact map_pow addMonoidAlgebraRingEquivDirectSum.symm f n

Result:
no goals

Proof state:
ι : Type u_1
M : Type u_3
inst✝³ : DecidableEq ι
inst✝² : AddMonoid ι
inst✝¹ : Semiring M
inst✝ : (m : M) → Decidable (m ≠ 0)
f : ⨁ (x : ι), M
n : ℕ
⊢ (f ^ n).toAddMonoidAlgebra = f.toAddMonoidAlgebra ^ n

Tactic:
exact map_pow addMonoidAlgebraRingEquivDirectSum.symm f n

Result:
no goals
-- Mathlib/Topology/MetricSpace/Pseudo/Defs.lean
theorem nndist_dist (x y : α) : nndist x y = Real.toNNReal (dist x y)

Proof state:
α : Type u
inst✝ : PseudoMetricSpace α
x y : α
⊢ nndist x y = (dist x y).toNNReal

Tactic:
rw [dist_nndist, Real.toNNReal_coe]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Complex/Arg.lean
@[simp] lemma arg_one : arg 1 = 0

Proof state:
⊢ arg 1 = 0

Tactic:
simp [arg, zero_le_one]

Result:
no goals
-- Mathlib/NumberTheory/Padics/PadicNumbers.lean
theorem mul (q r : ℚ_[p]) : ‖q * r‖ = ‖q‖ * ‖r‖

Proof state:
p : ℕ
hp : Fact (Nat.Prime p)
q r : ℚ_[p]
⊢ ‖q * r‖ = ‖q‖ * ‖r‖

Tactic:
simp [Norm.norm, map_mul]

Result:
no goals
-- Mathlib/Analysis/Fourier/FiniteAbelian/PontryaginDuality.lean
@[simp]
lemma complexBasis_apply (ψ : AddChar α ℂ) : complexBasis α ψ = ψ

Proof state:
α : Type u_1
inst✝¹ : AddCommGroup α
inst✝ : Finite α
ψ : AddChar α ℂ
⊢ (complexBasis α) ψ = ⇑ψ

Tactic:
rw [coe_complexBasis]

Result:
no goals
-- Mathlib/Algebra/Lie/Weights/Basic.lean
lemma mem_posFittingComp (m : M) :
    m ∈ posFittingComp R L M ↔ m ∈ ⨆ (x : L), posFittingCompOf R M x

Proof state:
R : Type u_2
L : Type u_3
M : Type u_4
inst✝⁷ : CommRing R
inst✝⁶ : LieRing L
inst✝⁵ : LieAlgebra R L
inst✝⁴ : AddCommGroup M
inst✝³ : Module R M
inst✝² : LieRingModule L M
inst✝¹ : LieModule R L M
inst✝ : LieRing.IsNilpotent L
m : M
⊢ m ∈ posFittingComp R L M ↔ m ∈ ⨆ x, posFittingCompOf R M x

Tactic:
rfl

Result:
no goals
-- Mathlib/Algebra/Order/Module/Defs.lean
lemma pos_of_smul_pos_right [SMulPosReflectLT α β] (h : 0 < a • b) (hb : 0 ≤ b) : 0 < a :=
  lt_of_smul_lt_smul_right (by rwa [zero_smul]) hb

Proof state:
α : Type u_1
β : Type u_2
a : α
b : β
inst✝⁵ : Zero α
inst✝⁴ : Zero β
inst✝³ : SMulWithZero α β
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : SMulPosReflectLT α β
h : 0 < a • b
hb : 0 ≤ b
⊢ 0 • b < a • b

Tactic:
rwa [zero_smul]

Result:
no goals
-- Mathlib/Data/Real/Archimedean.lean
/-- As `sInf s = 0` when `s` is a set of reals that's either empty or unbounded below,
it suffices to show that all elements of `s` are nonpositive to show that `sInf s ≤ 0`. -/
lemma sInf_nonpos (hs : ∀ x ∈ s, x ≤ 0) : sInf s ≤ 0

Proof state:
case inl
hs : ∀ x ∈ ∅, x ≤ 0
⊢ sInf ∅ ≤ 0

Tactic:
exact sInf_empty.le

Result:
no goals

Proof state:
s : Set ℝ
hs : ∀ x ∈ s, x ≤ 0
⊢ sInf s ≤ 0

Tactic:
obtain rfl | ⟨x, hx⟩ := s.eq_empty_or_nonempty

Result:
case inl
hs : ∀ x ∈ ∅, x ≤ 0
⊢ sInf ∅ ≤ 0

case inr.intro
s : Set ℝ
hs : ∀ x ∈ s, x ≤ 0
x : ℝ
hx : x ∈ s
⊢ sInf s ≤ 0

Proof state:
case inr.intro
s : Set ℝ
hs : ∀ x ∈ s, x ≤ 0
x : ℝ
hx : x ∈ s
⊢ sInf s ≤ 0

Tactic:
exact sInf_nonpos' ⟨x, hx, hs _ hx⟩

Result:
no goals
-- Mathlib/Data/Finset/Option.lean
lemma forall_mem_eraseNone {s : Finset (Option α)} {p : Option α → Prop} :
    (∀ a ∈ eraseNone s, p a) ↔ ∀ a : α, (a : Option α) ∈ s → p a

Proof state:
α : Type u_1
s : Finset (Option α)
p : Option α → Prop
⊢ (∀ a ∈ eraseNone s, p (some a)) ↔ ∀ (a : α), some a ∈ s → p (some a)

Tactic:
simp [Option.forall]

Result:
no goals
-- Mathlib/Data/Set/Card.lean
theorem ncard_add_ncard_compl (s : Set α) (hs : s.Finite

Proof state:
α : Type u_1
s : Set α
hs : autoParam s.Finite _auto✝
hsc : autoParam sᶜ.Finite _auto✝
⊢ s.ncard + sᶜ.ncard = Nat.card α

Tactic:
rw [← ncard_univ, ← ncard_union_eq (@disjoint_compl_right _ _ s) hs hsc, union_compl_self]

Result:
no goals
-- Mathlib/Data/Set/Lattice.lean
theorem iInter_eq_compl_iUnion_compl (s : ι → Set β) : ⋂ i, s i = (⋃ i, (s i)ᶜ)ᶜ

Proof state:
β : Type u_2
ι : Sort u_5
s : ι → Set β
⊢ ⋂ i, s i = (⋃ i, (s i)ᶜ)ᶜ

Tactic:
simp only [compl_iUnion, compl_compl]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem shiftLeft_shiftLeft' {x : BitVec w₁} {y : BitVec w₂} {z : BitVec w₃} :
    x <<< y <<< z = x <<< (y.toNat + z.toNat)

Proof state:
w₁ w₂ w₃ : Nat
x : BitVec w₁
y : BitVec w₂
z : BitVec w₃
⊢ x <<< y <<< z = x <<< (y.toNat + z.toNat)

Tactic:
simp [shiftLeft_add]

Result:
no goals
-- Mathlib/Order/Filter/NAry.lean
theorem map₂_left_identity {f : α → β → β} {a : α} (h : ∀ b, f a b = b) (l : Filter β) :
    map₂ f (pure a) l = l

Proof state:
α : Type u_1
β : Type u_3
f : α → β → β
a : α
h : ∀ (b : β), f a b = b
l : Filter β
⊢ map₂ f (pure a) l = l

Tactic:
rw [map₂_pure_left, show f a = id from funext h, map_id]

Result:
no goals
-- Mathlib/Algebra/BigOperators/Group/Finset/Defs.lean
theorem disjoint_finset_sum_right {β : Type*} {i : Finset β} {f : β → Multiset α}
    {a : Multiset α} : Disjoint a (i.sum f) ↔ ∀ b ∈ i, Disjoint a (f b)

Proof state:
α : Type u_3
β : Type u_6
i : Finset β
f : β → Multiset α
a : Multiset α
⊢ Disjoint a (i.sum f) ↔ ∀ b ∈ i, Disjoint a (f b)

Tactic:
simpa only [disjoint_comm] using disjoint_finset_sum_left

Result:
no goals
-- Mathlib/RingTheory/AdicCompletion/Functoriality.lean
theorem map_comp (f : M →ₗ[R] N) (g : N →ₗ[R] P) :
    map I g ∘ₗ map I f = map I (g ∘ₗ f)

Proof state:
case h.h
R : Type u_1
inst✝⁶ : CommRing R
I : Ideal R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u_3
inst✝³ : AddCommGroup N
inst✝² : Module R N
P : Type u_4
inst✝¹ : AddCommGroup P
inst✝ : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
a✝ : AdicCauchySequence I M
n✝ : ℕ
⊢ ↑((map I g ∘ₗ map I f) ((mk I M) a✝)) n✝ = ↑((map I (g ∘ₗ f)) ((mk I M) a✝)) n✝

Tactic:
simp

Result:
no goals

Proof state:
R : Type u_1
inst✝⁶ : CommRing R
I : Ideal R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u_3
inst✝³ : AddCommGroup N
inst✝² : Module R N
P : Type u_4
inst✝¹ : AddCommGroup P
inst✝ : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
⊢ map I g ∘ₗ map I f = map I (g ∘ₗ f)

Tactic:
ext

Result:
case h.h
R : Type u_1
inst✝⁶ : CommRing R
I : Ideal R
M : Type u_2
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
N : Type u_3
inst✝³ : AddCommGroup N
inst✝² : Module R N
P : Type u_4
inst✝¹ : AddCommGroup P
inst✝ : Module R P
f : M →ₗ[R] N
g : N →ₗ[R] P
a✝ : AdicCauchySequence I M
n✝ : ℕ
⊢ ↑((map I g ∘ₗ map I f) ((mk I M) a✝)) n✝ = ↑((map I (g ∘ₗ f)) ((mk I M) a✝)) n✝
-- Mathlib/Algebra/Homology/SingleHomology.lean
@[reassoc (attr := simp)]
lemma singleObjCyclesSelfIso_inv_iCycles :
    (singleObjCyclesSelfIso _ _ _).inv ≫ ((single C c j).obj A).iCycles j =
      (singleObjXSelf c j A).inv

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : HasZeroMorphisms C
inst✝¹ : HasZeroObject C
ι : Type u_1
inst✝ : DecidableEq ι
c : ComplexShape ι
j : ι
A : C
⊢ (singleObjCyclesSelfIso c j A).inv ≫ ((single C c j).obj A).iCycles j = (singleObjXSelf c j A).inv

Tactic:
simp [singleObjCyclesSelfIso]

Result:
no goals
-- Mathlib/Algebra/Ring/NegOnePow.lean
@[simp]
lemma negOnePow_abs (n : ℤ) : |n|.negOnePow = n.negOnePow

Proof state:
n : ℤ
⊢ |n|.negOnePow = n.negOnePow

Tactic:
obtain h|h := abs_choice n <;> simp only [h, negOnePow_neg]

Result:
no goals
-- Mathlib/Data/Matroid/Basic.lean
theorem IsBase.exchange_mem {e : α}
    (hB₁ : M.IsBase B₁) (hB₂ : M.IsBase B₂) (hxB₁ : e ∈ B₁) (hxB₂ : e ∉ B₂) :
    ∃ y, (y ∈ B₂ ∧ y ∉ B₁) ∧ M.IsBase (insert y (B₁ \ {e}))

Proof state:
α : Type u_1
M : Matroid α
B₁ B₂ : Set α
e : α
hB₁ : M.IsBase B₁
hB₂ : M.IsBase B₂
hxB₁ : e ∈ B₁
hxB₂ : e ∉ B₂
⊢ ∃ y, (y ∈ B₂ ∧ y ∉ B₁) ∧ M.IsBase (insert y (B₁ \ {e}))

Tactic:
simpa using hB₁.exchange hB₂ ⟨hxB₁, hxB₂⟩

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Restrict.lean
theorem restrict_comm (hs : MeasurableSet s) :
    (μ.restrict t).restrict s = (μ.restrict s).restrict t

Proof state:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s t : Set α
hs : MeasurableSet s
⊢ (μ.restrict t).restrict s = (μ.restrict s).restrict t

Tactic:
rw [restrict_restrict hs, restrict_restrict' hs, inter_comm]

Result:
no goals
-- Mathlib/Data/Fintype/Basic.lean
theorem Fin.univ_map_def {n : ℕ} (f : Fin n ↪ α) :
    Finset.univ.map f = ⟨List.ofFn f, List.nodup_ofFn.mpr f.injective⟩

Proof state:
α : Type u_1
n : ℕ
f : Fin n ↪ α
⊢ map f univ = { val := ↑(List.ofFn ⇑f), nodup := ⋯ }

Tactic:
simp [Finset.map]

Result:
no goals
-- Mathlib/FieldTheory/SeparableClosure.lean
theorem separableClosure.comap_eq_of_algHom (i : E →ₐ[F] K) :
    (separableClosure F K).comap i = separableClosure F E

Proof state:
F : Type u
E : Type v
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
K : Type w
inst✝¹ : Field K
inst✝ : Algebra F K
i : E →ₐ[F] K
⊢ comap i (separableClosure F K) = separableClosure F E

Tactic:
ext x

Result:
case h
F : Type u
E : Type v
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
K : Type w
inst✝¹ : Field K
inst✝ : Algebra F K
i : E →ₐ[F] K
x : E
⊢ x ∈ comap i (separableClosure F K) ↔ x ∈ separableClosure F E

Proof state:
case h
F : Type u
E : Type v
inst✝⁴ : Field F
inst✝³ : Field E
inst✝² : Algebra F E
K : Type w
inst✝¹ : Field K
inst✝ : Algebra F K
i : E →ₐ[F] K
x : E
⊢ x ∈ comap i (separableClosure F K) ↔ x ∈ separableClosure F E

Tactic:
exact map_mem_separableClosure_iff i

Result:
no goals
-- Mathlib/Algebra/GeomSum.lean
theorem op_geom_sum (x : α) (n : ℕ) : op (∑ i ∈ range n, x ^ i) = ∑ i ∈ range n, op x ^ i

Proof state:
α : Type u
inst✝ : Semiring α
x : α
n : ℕ
⊢ op (∑ i ∈ range n, x ^ i) = ∑ i ∈ range n, op x ^ i

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/GroupWithZero/Divisibility.lean
theorem mul_dvd_mul_iff_left [CancelMonoidWithZero α] {a b c : α} (ha : a ≠ 0) :
    a * b ∣ a * c ↔ b ∣ c :=
  exists_congr fun d => by rw [mul_assoc, mul_right_inj' ha]

Proof state:
α : Type u_1
inst✝ : CancelMonoidWithZero α
a b c : α
ha : a ≠ 0
d : α
⊢ a * c = a * b * d ↔ c = b * d

Tactic:
rw [mul_assoc, mul_right_inj' ha]

Result:
no goals