harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean
theorem eLpNorm_indicator_sub_indicator (s t : Set α) (f : α → E) :
    eLpNorm (s.indicator f - t.indicator f) p μ = eLpNorm ((s ∆ t).indicator f) p μ :=
  eLpNorm_congr_norm_ae <| ae_of_all _ fun x ↦ by
    simp only [Pi.sub_apply, Set.apply_indicator_symmDiff norm_neg]

Proof state:
α : Type u_1
E : Type u_3
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
s t : Set α
f : α → E
x : α
⊢ ‖(s.indicator f - t.indicator f) x‖ = ‖(s ∆ t).indicator f x‖

Tactic:
simp only [Pi.sub_apply, Set.apply_indicator_symmDiff norm_neg]

Result:
no goals
-- Mathlib/RingTheory/Coprime/Lemmas.lean
theorem pow_left_iff (hm : 0 < m) : IsRelPrime (x ^ m) y ↔ IsRelPrime x y

Proof state:
α : Type u_1
inst✝¹ : CommMonoid α
inst✝ : DecompositionMonoid α
x y : α
m : ℕ
hm : 0 < m
⊢ IsRelPrime (x ^ m) y ↔ IsRelPrime x y

Tactic:
refine ⟨fun h ↦ ?_, IsRelPrime.pow_left⟩

Result:
α : Type u_1
inst✝¹ : CommMonoid α
inst✝ : DecompositionMonoid α
x y : α
m : ℕ
hm : 0 < m
h : IsRelPrime (x ^ m) y
⊢ IsRelPrime x y

Proof state:
α : Type u_1
inst✝¹ : CommMonoid α
inst✝ : DecompositionMonoid α
x y : α
m : ℕ
hm : 0 < m
h : IsRelPrime (∏ _x ∈ Finset.range m, x) y
⊢ IsRelPrime x y

Tactic:
exact h.of_prod_left 0 (Finset.mem_range.mpr hm)

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : CommMonoid α
inst✝ : DecompositionMonoid α
x y : α
m : ℕ
hm : 0 < m
h : IsRelPrime (x ^ m) y
⊢ IsRelPrime x y

Tactic:
rw [← Finset.card_range m, ← Finset.prod_const] at h

Result:
α : Type u_1
inst✝¹ : CommMonoid α
inst✝ : DecompositionMonoid α
x y : α
m : ℕ
hm : 0 < m
h : IsRelPrime (∏ _x ∈ Finset.range m, x) y
⊢ IsRelPrime x y
-- Mathlib/Order/Category/NonemptyFinLinOrd.lean
lemma id_apply (X : NonemptyFinLinOrd) (x : X) :
    (𝟙 X : X ⟶ X) x = x

Proof state:
X : NonemptyFinLinOrd
x : ↑X.toLinOrd
⊢ (ConcreteCategory.hom (𝟙 X)) x = x

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Module/ZMod.lean
theorem smul_mem (hx : x ∈ K) (c : ZMod n) : c • x ∈ K

Proof state:
n : ℕ
M : Type u_1
S : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module (ZMod n) M
inst✝¹ : SetLike S M
inst✝ : AddSubgroupClass S M
x : M
K : S
hx : x ∈ K
c : ZMod n
⊢ c • x ∈ K

Tactic:
rw [← ZMod.intCast_zmod_cast c, Int.cast_smul_eq_zsmul]

Result:
n : ℕ
M : Type u_1
S : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module (ZMod n) M
inst✝¹ : SetLike S M
inst✝ : AddSubgroupClass S M
x : M
K : S
hx : x ∈ K
c : ZMod n
⊢ c.cast • x ∈ K

Proof state:
n : ℕ
M : Type u_1
S : Type u_4
inst✝³ : AddCommGroup M
inst✝² : Module (ZMod n) M
inst✝¹ : SetLike S M
inst✝ : AddSubgroupClass S M
x : M
K : S
hx : x ∈ K
c : ZMod n
⊢ c.cast • x ∈ K

Tactic:
exact zsmul_mem hx (cast c)

Result:
no goals
-- Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean
lemma inv_mul_lt_one₀ (ha : 0 < a) : a⁻¹ * b < 1 ↔ b < a

Proof state:
G₀ : Type u_2
inst✝⁴ : GroupWithZero G₀
inst✝³ : PartialOrder G₀
inst✝² : ZeroLEOneClass G₀
inst✝¹ : PosMulReflectLT G₀
a b : G₀
inst✝ : PosMulStrictMono G₀
ha : 0 < a
⊢ a⁻¹ * b < 1 ↔ b < a

Tactic:
rw [inv_mul_lt_iff₀ ha, mul_one]

Result:
no goals
-- Mathlib/Dynamics/PeriodicPts/Defs.lean
theorem periodicOrbit_eq_nil_iff_not_periodic_pt :
    periodicOrbit f x = Cycle.nil ↔ x ∉ periodicPts f

Proof state:
α : Type u_1
f : α → α
x : α
⊢ minimalPeriod f x = 0 ↔ x ∉ periodicPts f

Tactic:
exact minimalPeriod_eq_zero_iff_nmem_periodicPts

Result:
no goals

Proof state:
α : Type u_1
f : α → α
x : α
⊢ periodicOrbit f x = Cycle.nil ↔ x ∉ periodicPts f

Tactic:
simp only [periodicOrbit.eq_1, Cycle.coe_eq_nil, List.map_eq_nil_iff, List.range_eq_nil]

Result:
α : Type u_1
f : α → α
x : α
⊢ minimalPeriod f x = 0 ↔ x ∉ periodicPts f
-- Mathlib/.lake/packages/batteries/Batteries/Data/String/Lemmas.lean
theorem back_eq (s : String) : back s = s.1.getLastD default

Proof state:
s : String
⊢ s.back = s.data.getLastD default

Tactic:
match s, s.1.eq_nil_or_concat with
| ⟨_⟩, .inl rfl => rfl
| ⟨_⟩, .inr ⟨cs, c, rfl⟩ => simp [back, prev_of_valid, get_of_valid]

Result:
no goals

Proof state:
s : String
cs : List Char
c : Char
⊢ { data := cs.concat c }.back = { data := cs.concat c }.data.getLastD default

Tactic:
simp [back, prev_of_valid, get_of_valid]

Result:
no goals

Proof state:
s : String
⊢ { data := [] }.back = { data := [] }.data.getLastD default

Tactic:
rfl

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/BitVec/Lemmas.lean
theorem zero_append_zero : 0#v ++ 0#w = 0#(v + w)

Proof state:
v w : Nat
⊢ 0#v ++ 0#w = 0#(v + w)

Tactic:
ext

Result:
case pred
v w i✝ : Nat
a✝ : i✝ < v + w
⊢ (0#v ++ 0#w).getLsbD i✝ = (0#(v + w)).getLsbD i✝

Proof state:
case pred
v w i✝ : Nat
a✝ : i✝ < v + w
⊢ (0#v ++ 0#w).getLsbD i✝ = (0#(v + w)).getLsbD i✝

Tactic:
simp only [getLsbD_append, getLsbD_zero, ite_self]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Complex/Arg.lean
theorem continuousAt_arg (h : x ∈ slitPlane) : ContinuousAt arg x

Proof state:
case inl
x : ℂ
h₀ : ‖x‖ ≠ 0
hx_re : 0 < x.re
⊢ ContinuousAt arg x

case inr.inl
x : ℂ
h₀ : ‖x‖ ≠ 0
hx_im : x.im < 0
⊢ ContinuousAt arg x

case inr.inr
x : ℂ
h₀ : ‖x‖ ≠ 0
hx_im : 0 < x.im
⊢ ContinuousAt arg x

Tactic:
exacts [(Real.continuousAt_arcsin.comp
        (continuous_im.continuousAt.div continuous_norm.continuousAt h₀)).congr
    (arg_eq_nhds_of_re_pos hx_re).symm,
  (Real.continuous_arccos.continuousAt.comp
          (continuous_re.continuousAt.div continuous_norm.continuousAt h₀)).neg.congr
    (arg_eq_nhds_of_im_neg hx_im).symm,
  (Real.continuous_arccos.continuousAt.comp
        (continuous_re.continuousAt.div continuous_norm.continuousAt h₀)).congr
    (arg_eq_nhds_of_im_pos hx_im).symm]

Result:
no goals

Proof state:
x : ℂ
h : x ∈ slitPlane
⊢ x ≠ 0

Tactic:
exact slitPlane_ne_zero h

Result:
no goals

Proof state:
x : ℂ
h : x ∈ slitPlane
⊢ ‖x‖ ≠ 0

Tactic:
rw [norm_ne_zero_iff]

Result:
x : ℂ
h : x ∈ slitPlane
⊢ x ≠ 0

Proof state:
x : ℂ
h : 0 < x.re ∨ x.im < 0 ∨ 0 < x.im
h₀ : ‖x‖ ≠ 0
⊢ ContinuousAt arg x

Tactic:
rcases h with (hx_re | hx_im | hx_im)

Result:
case inl
x : ℂ
h₀ : ‖x‖ ≠ 0
hx_re : 0 < x.re
⊢ ContinuousAt arg x

case inr.inl
x : ℂ
h₀ : ‖x‖ ≠ 0
hx_im : x.im < 0
⊢ ContinuousAt arg x

case inr.inr
x : ℂ
h₀ : ‖x‖ ≠ 0
hx_im : 0 < x.im
⊢ ContinuousAt arg x

Proof state:
x : ℂ
h : x ∈ slitPlane
h₀ : ‖x‖ ≠ 0
⊢ ContinuousAt arg x

Tactic:
rw [mem_slitPlane_iff, ← lt_or_lt_iff_ne] at h

Result:
x : ℂ
h : 0 < x.re ∨ x.im < 0 ∨ 0 < x.im
h₀ : ‖x‖ ≠ 0
⊢ ContinuousAt arg x

Proof state:
x : ℂ
h : x ∈ slitPlane
⊢ ContinuousAt arg x

Tactic:
have h₀ : ‖x‖ ≠ 0 := by
  rw [norm_ne_zero_iff]
  exact slitPlane_ne_zero h

Result:
x : ℂ
h : x ∈ slitPlane
h₀ : ‖x‖ ≠ 0
⊢ ContinuousAt arg x
-- Mathlib/CategoryTheory/Monoidal/Category.lean
theorem inv_hom_id_tensor' {V W X Y Z : C} (f : V ⟶ W) [IsIso f] (g : X ⟶ Y) (h : Y ⟶ Z) :
    (inv f ⊗ g) ≫ (f ⊗ h) = (𝟙 W ⊗ g) ≫ (𝟙 W ⊗ h)

Proof state:
C : Type u
𝒞 : Category.{v, u} C
inst✝¹ : MonoidalCategory C
V W X Y Z : C
f : V ⟶ W
inst✝ : IsIso f
g : X ⟶ Y
h : Y ⟶ Z
⊢ (inv f ⊗ g) ≫ (f ⊗ h) = (𝟙 W ⊗ g) ≫ (𝟙 W ⊗ h)

Tactic:
rw [← tensor_comp, IsIso.inv_hom_id]

Result:
C : Type u
𝒞 : Category.{v, u} C
inst✝¹ : MonoidalCategory C
V W X Y Z : C
f : V ⟶ W
inst✝ : IsIso f
g : X ⟶ Y
h : Y ⟶ Z
⊢ 𝟙 W ⊗ g ≫ h = (𝟙 W ⊗ g) ≫ (𝟙 W ⊗ h)

Proof state:
C : Type u
𝒞 : Category.{v, u} C
inst✝¹ : MonoidalCategory C
V W X Y Z : C
f : V ⟶ W
inst✝ : IsIso f
g : X ⟶ Y
h : Y ⟶ Z
⊢ 𝟙 W ⊗ g ≫ h = (𝟙 W ⊗ g) ≫ (𝟙 W ⊗ h)

Tactic:
simp [id_tensorHom]

Result:
no goals
-- Mathlib/Topology/ContinuousMap/Compact.lean
theorem dist_lt_iff_of_nonempty [Nonempty α] : dist f g < C ↔ ∀ x : α, dist (f x) (g x) < C

Proof state:
α : Type u_1
β : Type u_2
inst✝³ : TopologicalSpace α
inst✝² : CompactSpace α
inst✝¹ : PseudoMetricSpace β
f g : C(α, β)
C : ℝ
inst✝ : Nonempty α
⊢ dist f g < C ↔ ∀ (x : α), dist (f x) (g x) < C

Tactic:
simp only [← dist_mkOfCompact, dist_lt_iff_of_nonempty_compact, mkOfCompact_apply]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Degree/Operations.lean
theorem natDegree_sub_C {a : R} : natDegree (p - C a) = natDegree p

Proof state:
R : Type u
inst✝ : Ring R
p : R[X]
a : R
⊢ (p - C a).natDegree = p.natDegree

Tactic:
rw [sub_eq_add_neg, ← C_neg, natDegree_add_C]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Complex/Arg.lean
theorem arg_mul_cos_add_sin_mul_I_sub {r : ℝ} (hr : 0 < r) (θ : ℝ) :
    arg (r * (cos θ + sin θ * I)) - θ = 2 * π * ⌊(π - θ) / (2 * π)⌋

Proof state:
r : ℝ
hr : 0 < r
θ : ℝ
⊢ ↑(- -⌊(-π + 2 * π - θ) / (2 * π)⌋) * (2 * π) = 2 * π * ↑⌊(π - θ) / (2 * π)⌋

Tactic:
ring_nf

Result:
no goals

Proof state:
r : ℝ
hr : 0 < r
θ : ℝ
⊢ (↑r * (cos ↑θ + sin ↑θ * I)).arg - θ = 2 * π * ↑⌊(π - θ) / (2 * π)⌋

Tactic:
rw [arg_mul_cos_add_sin_mul_I_eq_toIocMod hr, toIocMod_sub_self, toIocDiv_eq_neg_floor,
  zsmul_eq_mul]

Result:
r : ℝ
hr : 0 < r
θ : ℝ
⊢ ↑(- -⌊(-π + 2 * π - θ) / (2 * π)⌋) * (2 * π) = 2 * π * ↑⌊(π - θ) / (2 * π)⌋
-- Mathlib/Data/Finsupp/Basic.lean
theorem frange_single {x : α} {y : M} : frange (single x y) ⊆ {y} := fun r hr =>
  let ⟨t, ht1, ht2⟩ := mem_frange.1 hr
  ht2 ▸ by
    classical
      rw [single_apply] at ht2 ⊢
      split_ifs at ht2 ⊢
      · exact Finset.mem_singleton_self _
      · exact (t ht2.symm).elim

Proof state:
α : Type u_1
M : Type u_5
inst✝ : Zero M
x : α
y r : M
hr : r ∈ (single x y).frange
t : r ≠ 0
ht1 : α
ht2 : (single x y) ht1 = r
⊢ (single x y) ht1 ∈ {y}

Tactic:
rw [single_apply] at ht2 ⊢

Result:
α : Type u_1
M : Type u_5
inst✝ : Zero M
x : α
y r : M
hr : r ∈ (single x y).frange
t : r ≠ 0
ht1 : α
ht2 : (if x = ht1 then y else 0) = r
⊢ (if x = ht1 then y else 0) ∈ {y}

Proof state:
case pos
α : Type u_1
M : Type u_5
inst✝ : Zero M
x : α
y r : M
hr : r ∈ (single x y).frange
t : r ≠ 0
ht1 : α
h✝ : x = ht1
ht2 : y = r
⊢ y ∈ {y}

Tactic:
exact Finset.mem_singleton_self _

Result:
no goals

Proof state:
α : Type u_1
M : Type u_5
inst✝ : Zero M
x : α
y r : M
hr : r ∈ (single x y).frange
t : r ≠ 0
ht1 : α
ht2 : (if x = ht1 then y else 0) = r
⊢ (if x = ht1 then y else 0) ∈ {y}

Tactic:
split_ifs at ht2 ⊢

Result:
case pos
α : Type u_1
M : Type u_5
inst✝ : Zero M
x : α
y r : M
hr : r ∈ (single x y).frange
t : r ≠ 0
ht1 : α
h✝ : x = ht1
ht2 : y = r
⊢ y ∈ {y}

case neg
α : Type u_1
M : Type u_5
inst✝ : Zero M
x : α
y r : M
hr : r ∈ (single x y).frange
t : r ≠ 0
ht1 : α
h✝ : ¬x = ht1
ht2 : 0 = r
⊢ 0 ∈ {y}

Proof state:
case neg
α : Type u_1
M : Type u_5
inst✝ : Zero M
x : α
y r : M
hr : r ∈ (single x y).frange
t : r ≠ 0
ht1 : α
h✝ : ¬x = ht1
ht2 : 0 = r
⊢ 0 ∈ {y}

Tactic:
exact (t ht2.symm).elim

Result:
no goals
-- Mathlib/Analysis/CStarAlgebra/Spectrum.lean
theorem IsSelfAdjoint.spectralRadius_eq_nnnorm {a : A} (ha : IsSelfAdjoint a) :
    spectralRadius ℂ a = ‖a‖₊

Proof state:
case h.e'_3
A : Type u_1
inst✝ : CStarAlgebra A
a : A
ha : IsSelfAdjoint a
hconst : Tendsto (fun _n => ↑‖a‖₊) atTop (𝓝 ↑‖a‖₊)
n : ℕ
⊢ ↑‖a‖₊ = ↑‖a‖₊ ^ (↑(2 ^ n) * (1 / ↑(2 ^ n)))

Tactic:
simp

Result:
no goals

Proof state:
case h.e'_3
A : Type u_1
inst✝ : CStarAlgebra A
a : A
ha : IsSelfAdjoint a
hconst : Tendsto (fun _n => ↑‖a‖₊) atTop (𝓝 ↑‖a‖₊)
n : ℕ
⊢ ↑‖a‖₊ = ((fun n => ↑‖a ^ n‖₊ ^ (1 / ↑n)) ∘ fun n => 2 ^ n) n

Tactic:
rw [Function.comp_apply, ha.nnnorm_pow_two_pow, ENNReal.coe_pow, ← rpow_natCast, ← rpow_mul]

Result:
case h.e'_3
A : Type u_1
inst✝ : CStarAlgebra A
a : A
ha : IsSelfAdjoint a
hconst : Tendsto (fun _n => ↑‖a‖₊) atTop (𝓝 ↑‖a‖₊)
n : ℕ
⊢ ↑‖a‖₊ = ↑‖a‖₊ ^ (↑(2 ^ n) * (1 / ↑(2 ^ n)))

Proof state:
A : Type u_1
inst✝ : CStarAlgebra A
a : A
ha : IsSelfAdjoint a
⊢ spectralRadius ℂ a = ↑‖a‖₊

Tactic:
have hconst : Tendsto (fun _n : ℕ => (‖a‖₊ : ℝ≥0∞)) atTop _ := tendsto_const_nhds

Result:
A : Type u_1
inst✝ : CStarAlgebra A
a : A
ha : IsSelfAdjoint a
hconst : Tendsto (fun _n => ↑‖a‖₊) atTop (𝓝 ↑‖a‖₊)
⊢ spectralRadius ℂ a = ↑‖a‖₊

Proof state:
case h.e'_3
A : Type u_1
inst✝ : CStarAlgebra A
a : A
ha : IsSelfAdjoint a
hconst : Tendsto (fun _n => ↑‖a‖₊) atTop (𝓝 ↑‖a‖₊)
⊢ (fun _n => ↑‖a‖₊) = (fun n => ↑‖a ^ n‖₊ ^ (1 / ↑n)) ∘ fun n => 2 ^ n

Tactic:
refine funext fun n => ?_

Result:
case h.e'_3
A : Type u_1
inst✝ : CStarAlgebra A
a : A
ha : IsSelfAdjoint a
hconst : Tendsto (fun _n => ↑‖a‖₊) atTop (𝓝 ↑‖a‖₊)
n : ℕ
⊢ ↑‖a‖₊ = ((fun n => ↑‖a ^ n‖₊ ^ (1 / ↑n)) ∘ fun n => 2 ^ n) n

Proof state:
A : Type u_1
inst✝ : CStarAlgebra A
a : A
ha : IsSelfAdjoint a
hconst : Tendsto (fun _n => ↑‖a‖₊) atTop (𝓝 ↑‖a‖₊)
⊢ Tendsto (fun _n => ↑‖a‖₊) atTop (𝓝 (spectralRadius ℂ a))

Tactic:
convert
  (spectrum.pow_nnnorm_pow_one_div_tendsto_nhds_spectralRadius (a : A)).comp
    (Nat.tendsto_pow_atTop_atTop_of_one_lt one_lt_two) using 1

Result:
case h.e'_3
A : Type u_1
inst✝ : CStarAlgebra A
a : A
ha : IsSelfAdjoint a
hconst : Tendsto (fun _n => ↑‖a‖₊) atTop (𝓝 ↑‖a‖₊)
⊢ (fun _n => ↑‖a‖₊) = (fun n => ↑‖a ^ n‖₊ ^ (1 / ↑n)) ∘ fun n => 2 ^ n

Proof state:
A : Type u_1
inst✝ : CStarAlgebra A
a : A
ha : IsSelfAdjoint a
hconst : Tendsto (fun _n => ↑‖a‖₊) atTop (𝓝 ↑‖a‖₊)
⊢ spectralRadius ℂ a = ↑‖a‖₊

Tactic:
refine tendsto_nhds_unique ?_ hconst

Result:
A : Type u_1
inst✝ : CStarAlgebra A
a : A
ha : IsSelfAdjoint a
hconst : Tendsto (fun _n => ↑‖a‖₊) atTop (𝓝 ↑‖a‖₊)
⊢ Tendsto (fun _n => ↑‖a‖₊) atTop (𝓝 (spectralRadius ℂ a))
-- Mathlib/Algebra/Polynomial/Basic.lean
theorem card_support_eq_zero : #p.support = 0 ↔ p = 0

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
⊢ #p.support = 0 ↔ p = 0

Tactic:
simp

Result:
no goals
-- Mathlib/LinearAlgebra/Multilinear/Pi.lean
theorem piFamily_smul
    [Monoid S] [∀ p, DistribMulAction S (N p)] [∀ p, SMulCommClass R S (N p)]
    (s : S) (f : Π (p : Π i, κ i), MultilinearMap R (fun i ↦ M i (p i)) (N p)) :
    piFamily (s • f) = s • piFamily f

Proof state:
ι : Type uι
κ : ι → Type uκ
S : Type uS
R : Type uR
M : (i : ι) → κ i → Type uM
N : ((i : ι) → κ i) → Type uN
inst✝⁷ : Semiring R
inst✝⁶ : (i : ι) → (k : κ i) → AddCommMonoid (M i k)
inst✝⁵ : (p : (i : ι) → κ i) → AddCommMonoid (N p)
inst✝⁴ : (i : ι) → (k : κ i) → Module R (M i k)
inst✝³ : (p : (i : ι) → κ i) → Module R (N p)
inst✝² : Monoid S
inst✝¹ : (p : (i : ι) → κ i) → DistribMulAction S (N p)
inst✝ : ∀ (p : (i : ι) → κ i), SMulCommClass R S (N p)
s : S
f : (p : (i : ι) → κ i) → MultilinearMap R (fun i => M i (p i)) (N p)
⊢ piFamily (s • f) = s • piFamily f

Tactic:
ext

Result:
case H.h
ι : Type uι
κ : ι → Type uκ
S : Type uS
R : Type uR
M : (i : ι) → κ i → Type uM
N : ((i : ι) → κ i) → Type uN
inst✝⁷ : Semiring R
inst✝⁶ : (i : ι) → (k : κ i) → AddCommMonoid (M i k)
inst✝⁵ : (p : (i : ι) → κ i) → AddCommMonoid (N p)
inst✝⁴ : (i : ι) → (k : κ i) → Module R (M i k)
inst✝³ : (p : (i : ι) → κ i) → Module R (N p)
inst✝² : Monoid S
inst✝¹ : (p : (i : ι) → κ i) → DistribMulAction S (N p)
inst✝ : ∀ (p : (i : ι) → κ i), SMulCommClass R S (N p)
s : S
f : (p : (i : ι) → κ i) → MultilinearMap R (fun i => M i (p i)) (N p)
x✝¹ : (i : ι) → (j : κ i) → M i j
x✝ : (i : ι) → κ i
⊢ (piFamily (s • f)) x✝¹ x✝ = (s • piFamily f) x✝¹ x✝

Proof state:
case H.h
ι : Type uι
κ : ι → Type uκ
S : Type uS
R : Type uR
M : (i : ι) → κ i → Type uM
N : ((i : ι) → κ i) → Type uN
inst✝⁷ : Semiring R
inst✝⁶ : (i : ι) → (k : κ i) → AddCommMonoid (M i k)
inst✝⁵ : (p : (i : ι) → κ i) → AddCommMonoid (N p)
inst✝⁴ : (i : ι) → (k : κ i) → Module R (M i k)
inst✝³ : (p : (i : ι) → κ i) → Module R (N p)
inst✝² : Monoid S
inst✝¹ : (p : (i : ι) → κ i) → DistribMulAction S (N p)
inst✝ : ∀ (p : (i : ι) → κ i), SMulCommClass R S (N p)
s : S
f : (p : (i : ι) → κ i) → MultilinearMap R (fun i => M i (p i)) (N p)
x✝¹ : (i : ι) → (j : κ i) → M i j
x✝ : (i : ι) → κ i
⊢ (piFamily (s • f)) x✝¹ x✝ = (s • piFamily f) x✝¹ x✝

Tactic:
simp

Result:
no goals
-- Mathlib/MeasureTheory/OuterMeasure/AE.lean
theorem measure_symmDiff_eq_zero_iff {s t : Set α} : μ (s ∆ t) = 0 ↔ s =ᵐ[μ] t

Proof state:
α : Type u_1
F : Type u_3
inst✝¹ : FunLike F (Set α) ℝ≥0∞
inst✝ : OuterMeasureClass F α
μ : F
s t : Set α
⊢ μ (s ∆ t) = 0 ↔ s =ᶠ[ae μ] t

Tactic:
simp [ae_eq_set, symmDiff_def]

Result:
no goals
-- Mathlib/Data/PNat/Factors.lean
theorem prod_add (u v : PrimeMultiset) : (u + v).prod = u.prod * v.prod

Proof state:
u v : PrimeMultiset
⊢ (coePNatMonoidHom u + coePNatMonoidHom v).prod = u.prod * v.prod

Tactic:
exact Multiset.prod_add _ _

Result:
no goals

Proof state:
u v : PrimeMultiset
⊢ (u + v).prod = u.prod * v.prod

Tactic:
change (coePNatMonoidHom (u + v)).prod = _

Result:
u v : PrimeMultiset
⊢ (coePNatMonoidHom (u + v)).prod = u.prod * v.prod

Proof state:
u v : PrimeMultiset
⊢ (coePNatMonoidHom (u + v)).prod = u.prod * v.prod

Tactic:
rw [coePNatMonoidHom.map_add]

Result:
u v : PrimeMultiset
⊢ (coePNatMonoidHom u + coePNatMonoidHom v).prod = u.prod * v.prod
-- Mathlib/LinearAlgebra/QuadraticForm/Basic.lean
theorem associated_left_inverse {B₁ : BilinMap R M N} (h : ∀ x y, B₁ x y = B₁ y x) :
    associatedHom S B₁.toQuadraticMap = B₁ :=
  LinearMap.ext₂ fun x y ↦ by
    rw [associated_toQuadraticMap, ← h x y, ← two_smul R, invOf_smul_eq_iff, two_smul, two_smul]

Proof state:
S : Type u_1
R : Type u_3
M : Type u_4
N : Type u_5
inst✝⁹ : CommRing R
inst✝⁸ : AddCommGroup M
inst✝⁷ : Module R M
inst✝⁶ : AddCommGroup N
inst✝⁵ : Module R N
inst✝⁴ : CommSemiring S
inst✝³ : Algebra S R
inst✝² : Module S N
inst✝¹ : IsScalarTower S R N
inst✝ : Invertible 2
B₁ : BilinMap R M N
h : ∀ (x y : M), (B₁ x) y = (B₁ y) x
x y : M
⊢ (((associatedHom S) B₁.toQuadraticMap) x) y = (B₁ x) y

Tactic:
rw [associated_toQuadraticMap, ← h x y, ← two_smul R, invOf_smul_eq_iff, two_smul, two_smul]

Result:
no goals
-- Mathlib/RingTheory/IsAdjoinRoot.lean
theorem basis_apply (h : IsAdjoinRootMonic S f) (i) : h.basis i = h.root ^ (i : ℕ) :=
  Basis.apply_eq_iff.mpr <|
    show (h.modByMonicHom (h.toIsAdjoinRoot.root ^ (i : ℕ))).toFinsupp.comapDomain _
          Fin.val_injective.injOn = Finsupp.single _ _ by
      ext j
      rw [Finsupp.comapDomain_apply, modByMonicHom_root_pow]
      · rw [X_pow_eq_monomial, toFinsupp_monomial, Finsupp.single_apply_left Fin.val_injective]
      · exact i.is_lt

Proof state:
case h
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
f : R[X]
inst✝ : Algebra R S
h : IsAdjoinRootMonic S f
i j : Fin f.natDegree
⊢ (Finsupp.comapDomain Fin.val (h.modByMonicHom (h.root ^ ↑i)).toFinsupp ⋯) j = (Finsupp.single i 1) j

Tactic:
rw [Finsupp.comapDomain_apply, modByMonicHom_root_pow]

Result:
case h
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
f : R[X]
inst✝ : Algebra R S
h : IsAdjoinRootMonic S f
i j : Fin f.natDegree
⊢ (X ^ ↑i).toFinsupp ↑j = (Finsupp.single i 1) j

case h.hdeg
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
f : R[X]
inst✝ : Algebra R S
h : IsAdjoinRootMonic S f
i j : Fin f.natDegree
⊢ ↑i < f.natDegree

Proof state:
case h
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
f : R[X]
inst✝ : Algebra R S
h : IsAdjoinRootMonic S f
i j : Fin f.natDegree
⊢ (X ^ ↑i).toFinsupp ↑j = (Finsupp.single i 1) j

Tactic:
rw [X_pow_eq_monomial, toFinsupp_monomial, Finsupp.single_apply_left Fin.val_injective]

Result:
no goals

Proof state:
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
f : R[X]
inst✝ : Algebra R S
h : IsAdjoinRootMonic S f
i : Fin f.natDegree
⊢ Finsupp.comapDomain Fin.val (h.modByMonicHom (h.root ^ ↑i)).toFinsupp ⋯ = Finsupp.single i 1

Tactic:
ext j

Result:
case h
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
f : R[X]
inst✝ : Algebra R S
h : IsAdjoinRootMonic S f
i j : Fin f.natDegree
⊢ (Finsupp.comapDomain Fin.val (h.modByMonicHom (h.root ^ ↑i)).toFinsupp ⋯) j = (Finsupp.single i 1) j

Proof state:
case h.hdeg
R : Type u
S : Type v
inst✝² : CommRing R
inst✝¹ : Ring S
f : R[X]
inst✝ : Algebra R S
h : IsAdjoinRootMonic S f
i j : Fin f.natDegree
⊢ ↑i < f.natDegree

Tactic:
exact i.is_lt

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/Ideal.lean
theorem matricesOver_top : (⊤ : Ideal R).matricesOver n = ⊤

Proof state:
case h
R : Type u_1
inst✝² : Semiring R
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
x✝ : Matrix n n R
⊢ x✝ ∈ matricesOver n ⊤ ↔ x✝ ∈ ⊤

Tactic:
simp

Result:
no goals

Proof state:
R : Type u_1
inst✝² : Semiring R
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
⊢ matricesOver n ⊤ = ⊤

Tactic:
ext

Result:
case h
R : Type u_1
inst✝² : Semiring R
n : Type u_2
inst✝¹ : Fintype n
inst✝ : DecidableEq n
x✝ : Matrix n n R
⊢ x✝ ∈ matricesOver n ⊤ ↔ x✝ ∈ ⊤
-- Mathlib/LinearAlgebra/Dimension/Constructions.lean
theorem rank_tensorProduct :
    Module.rank R (M ⊗[S] M') =
      Cardinal.lift.{v'} (Module.rank R M) * Cardinal.lift.{v} (Module.rank S M')

Proof state:
case intro.mk
R : Type u
S : Type u'
M : Type v
M' : Type v'
inst✝¹² : Semiring R
inst✝¹¹ : CommSemiring S
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : AddCommMonoid M'
inst✝⁸ : Module R M
inst✝⁷ : StrongRankCondition R
inst✝⁶ : StrongRankCondition S
inst✝⁵ : Module S M
inst✝⁴ : Module S M'
inst✝³ : Free S M'
inst✝² : Algebra S R
inst✝¹ : IsScalarTower S R M
inst✝ : Free R M
fst✝ : Type v
bM : Basis fst✝ R M
⊢ Module.rank R (M ⊗[S] M') = Cardinal.lift.{v', v} (Module.rank R M) * Cardinal.lift.{v, v'} (Module.rank S M')

Tactic:
obtain ⟨⟨_, bN⟩⟩ := Module.Free.exists_basis (R := S) (M := M')

Result:
case intro.mk.intro.mk
R : Type u
S : Type u'
M : Type v
M' : Type v'
inst✝¹² : Semiring R
inst✝¹¹ : CommSemiring S
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : AddCommMonoid M'
inst✝⁸ : Module R M
inst✝⁷ : StrongRankCondition R
inst✝⁶ : StrongRankCondition S
inst✝⁵ : Module S M
inst✝⁴ : Module S M'
inst✝³ : Free S M'
inst✝² : Algebra S R
inst✝¹ : IsScalarTower S R M
inst✝ : Free R M
fst✝¹ : Type v
bM : Basis fst✝¹ R M
fst✝ : Type v'
bN : Basis fst✝ S M'
⊢ Module.rank R (M ⊗[S] M') = Cardinal.lift.{v', v} (Module.rank R M) * Cardinal.lift.{v, v'} (Module.rank S M')

Proof state:
case intro.mk.intro.mk
R : Type u
S : Type u'
M : Type v
M' : Type v'
inst✝¹² : Semiring R
inst✝¹¹ : CommSemiring S
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : AddCommMonoid M'
inst✝⁸ : Module R M
inst✝⁷ : StrongRankCondition R
inst✝⁶ : StrongRankCondition S
inst✝⁵ : Module S M
inst✝⁴ : Module S M'
inst✝³ : Free S M'
inst✝² : Algebra S R
inst✝¹ : IsScalarTower S R M
inst✝ : Free R M
fst✝¹ : Type v
bM : Basis fst✝¹ R M
fst✝ : Type v'
bN : Basis fst✝ S M'
⊢ Module.rank R (M ⊗[S] M') = Cardinal.lift.{v', v} (Module.rank R M) * Cardinal.lift.{v, v'} (Module.rank S M')

Tactic:
rw [← bM.mk_eq_rank'', ← bN.mk_eq_rank'', ← (bM.tensorProduct bN).mk_eq_rank'', Cardinal.mk_prod]

Result:
no goals

Proof state:
R : Type u
S : Type u'
M : Type v
M' : Type v'
inst✝¹² : Semiring R
inst✝¹¹ : CommSemiring S
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : AddCommMonoid M'
inst✝⁸ : Module R M
inst✝⁷ : StrongRankCondition R
inst✝⁶ : StrongRankCondition S
inst✝⁵ : Module S M
inst✝⁴ : Module S M'
inst✝³ : Free S M'
inst✝² : Algebra S R
inst✝¹ : IsScalarTower S R M
inst✝ : Free R M
⊢ Module.rank R (M ⊗[S] M') = Cardinal.lift.{v', v} (Module.rank R M) * Cardinal.lift.{v, v'} (Module.rank S M')

Tactic:
obtain ⟨⟨_, bM⟩⟩ := Module.Free.exists_basis (R := R) (M := M)

Result:
case intro.mk
R : Type u
S : Type u'
M : Type v
M' : Type v'
inst✝¹² : Semiring R
inst✝¹¹ : CommSemiring S
inst✝¹⁰ : AddCommMonoid M
inst✝⁹ : AddCommMonoid M'
inst✝⁸ : Module R M
inst✝⁷ : StrongRankCondition R
inst✝⁶ : StrongRankCondition S
inst✝⁵ : Module S M
inst✝⁴ : Module S M'
inst✝³ : Free S M'
inst✝² : Algebra S R
inst✝¹ : IsScalarTower S R M
inst✝ : Free R M
fst✝ : Type v
bM : Basis fst✝ R M
⊢ Module.rank R (M ⊗[S] M') = Cardinal.lift.{v', v} (Module.rank R M) * Cardinal.lift.{v, v'} (Module.rank S M')