harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/RingTheory/Polynomial/Cyclotomic/Roots.lean
theorem _root_.IsPrimitiveRoot.isRoot_cyclotomic (hpos : 0 < n) {μ : R} (h : IsPrimitiveRoot μ n) :
    IsRoot (cyclotomic n R) μ

Proof state:
R : Type u_1
inst✝¹ : CommRing R
n : ℕ
inst✝ : IsDomain R
hpos : 0 < n
μ : R
h : IsPrimitiveRoot μ n
⊢ μ ∈ primitiveRoots n R

Tactic:
rwa [← mem_primitiveRoots hpos] at h

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : CommRing R
n : ℕ
inst✝ : IsDomain R
hpos : 0 < n
μ : R
h : IsPrimitiveRoot μ n
⊢ (cyclotomic n R).IsRoot μ

Tactic:
rw [← mem_roots (cyclotomic_ne_zero n R), cyclotomic_eq_prod_X_sub_primitiveRoots h,
  roots_prod_X_sub_C, ← Finset.mem_def]

Result:
R : Type u_1
inst✝¹ : CommRing R
n : ℕ
inst✝ : IsDomain R
hpos : 0 < n
μ : R
h : IsPrimitiveRoot μ n
⊢ μ ∈ primitiveRoots n R
-- Mathlib/Algebra/Polynomial/AlgebraMap.lean
theorem not_isUnit_X_sub_C [Nontrivial R] (r : R) : ¬IsUnit (X - C r) :=
  fun ⟨⟨_, g, _hfg, hgf⟩, rfl⟩ => zero_ne_one' R <| by rw [← eval_mul_X_sub_C, hgf, eval_one]

Proof state:
R : Type u
inst✝¹ : Ring R
inst✝ : Nontrivial R
r : R
x✝ : IsUnit (X - C r)
g : R[X]
_hfg : (X - C r) * g = 1
hgf : g * (X - C r) = 1
⊢ 0 = 1

Tactic:
rw [← eval_mul_X_sub_C, hgf, eval_one]

Result:
no goals
-- Mathlib/Topology/Constructions.lean
protected lemma Topology.IsOpenEmbedding.inclusion (hst : s ⊆ t) (hs : IsOpen (t ↓∩ s)) :
    IsOpenEmbedding (inclusion hst) where
  toIsEmbedding := .inclusion _
  isOpen_range

Proof state:
X : Type u
inst✝ : TopologicalSpace X
s t : Set X
hst : s ⊆ t
hs : IsOpen (t ↓∩ s)
⊢ IsOpen (range (inclusion hst))

Tactic:
rwa [range_inclusion]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/Transvection.lean
theorem listTransvecCol_getElem {i : ℕ} (h : i < (listTransvecCol M).length) :
    (listTransvecCol M)[i] =
      letI i' : Fin r := ⟨i, length_listTransvecCol M ▸ h⟩
      transvection (inl i') (inr unit) <| -M (inl i') (inr unit) / M (inr unit) (inr unit)

Proof state:
𝕜 : Type u_3
inst✝ : Field 𝕜
r : ℕ
M : Matrix (Fin r ⊕ Unit) (Fin r ⊕ Unit) 𝕜
i : ℕ
h : i < (listTransvecCol M).length
⊢ (listTransvecCol M)[i] = transvection (inl ⟨i, ⋯⟩) (inr ()) (-M (inl ⟨i, ⋯⟩) (inr ()) / M (inr ()) (inr ()))

Tactic:
simp [listTransvecCol]

Result:
no goals
-- Mathlib/Topology/Basic.lean
lemma interior_subset_iff : interior s ⊆ t ↔ ∀ U, IsOpen U → U ⊆ s → U ⊆ t

Proof state:
X : Type u
s t : Set X
inst✝ : TopologicalSpace X
⊢ interior s ⊆ t ↔ ∀ (U : Set X), IsOpen U → U ⊆ s → U ⊆ t

Tactic:
simp [interior]

Result:
no goals
-- Mathlib/SetTheory/Game/Nim.lean
theorem leftMoves_nim (o : Ordinal) : (nim o).LeftMoves = o.toType

Proof state:
o : Ordinal.{u_1}
⊢ (mk o.toType o.toType (fun x => nim ↑(o.enumIsoToType.symm x)) fun x => nim ↑(o.enumIsoToType.symm x)).LeftMoves =
    o.toType

Tactic:
rfl

Result:
no goals

Proof state:
o : Ordinal.{u_1}
⊢ (nim o).LeftMoves = o.toType

Tactic:
rw [nim]

Result:
o : Ordinal.{u_1}
⊢ (mk o.toType o.toType (fun x => nim ↑(o.enumIsoToType.symm x)) fun x => nim ↑(o.enumIsoToType.symm x)).LeftMoves =
    o.toType
-- Mathlib/Algebra/Group/Support.lean
theorem mulSupport_pow [Monoid M] (f : α → M) (n : ℕ) :
    (mulSupport fun x => f x ^ n) ⊆ mulSupport f

Proof state:
case zero
α : Type u_1
M : Type u_5
inst✝ : Monoid M
f : α → M
⊢ (mulSupport fun x => f x ^ 0) ⊆ mulSupport f

Tactic:
simp [pow_zero, mulSupport_one]

Result:
no goals

Proof state:
case succ
α : Type u_1
M : Type u_5
inst✝ : Monoid M
f : α → M
n : ℕ
hfn : (mulSupport fun x => f x ^ n) ⊆ mulSupport f
⊢ (mulSupport fun x => f x ^ (n + 1)) ⊆ mulSupport f

Tactic:
simpa only [pow_succ'] using (mulSupport_mul f _).trans (union_subset Subset.rfl hfn)

Result:
no goals

Proof state:
α : Type u_1
M : Type u_5
inst✝ : Monoid M
f : α → M
n : ℕ
⊢ (mulSupport fun x => f x ^ n) ⊆ mulSupport f

Tactic:
induction n with
| zero => simp [pow_zero, mulSupport_one]
| succ n hfn =>
  simpa only [pow_succ'] using (mulSupport_mul f _).trans (union_subset Subset.rfl hfn)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Count.lean
theorem countP_flatMap (p : β → Bool) (l : Array α) (f : α → Array β) :
    countP p (l.flatMap f) = sum (map (countP p ∘ f) l)

Proof state:
α : Type u_2
β : Type u_1
p : β → Bool
l : Array α
f : α → Array β
⊢ countP p (flatMap f l) = (map (countP p ∘ f) l).sum

Tactic:
cases l

Result:
case mk
α : Type u_2
β : Type u_1
p : β → Bool
f : α → Array β
toList✝ : List α
⊢ countP p (flatMap f { toList := toList✝ }) = (map (countP p ∘ f) { toList := toList✝ }).sum

Proof state:
case mk
α : Type u_2
β : Type u_1
p : β → Bool
f : α → Array β
toList✝ : List α
⊢ countP p (flatMap f { toList := toList✝ }) = (map (countP p ∘ f) { toList := toList✝ }).sum

Tactic:
simp [List.countP_flatMap, Function.comp_def]

Result:
no goals
-- Mathlib/Algebra/Module/LocalizedModule/Basic.lean
theorem mul_by_divBy (s : S) (p : LocalizedModule S M) :
    algebraMap R (Module.End R (LocalizedModule S M)) s (divBy s p) = p :=
  p.induction_on fun m t => by
    rw [divBy_apply, Module.algebraMap_end_apply, LocalizedModule.liftOn_mk, smul'_mk,
      ← Submonoid.smul_def, mk_cancel_common_right _ s]

Proof state:
R : Type u
inst✝² : CommSemiring R
S : Submonoid R
M : Type v
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
s : ↥S
p : LocalizedModule S M
m : M
t : ↥S
⊢ ((algebraMap R (Module.End R (LocalizedModule S M))) ↑s) ((divBy s) (mk m t)) = mk m t

Tactic:
rw [divBy_apply, Module.algebraMap_end_apply, LocalizedModule.liftOn_mk, smul'_mk,
  ← Submonoid.smul_def, mk_cancel_common_right _ s]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/String/Basic.lean
theorem addChar_right_comm (p : Pos) (c₁ c₂ : Char) : p + c₁ + c₂ = p + c₂ + c₁

Proof state:
p : Pos
c₁ c₂ : Char
⊢ p + c₁ + c₂ = p + c₂ + c₁

Tactic:
apply ext

Result:
case h
p : Pos
c₁ c₂ : Char
⊢ (p + c₁ + c₂).byteIdx = (p + c₂ + c₁).byteIdx

Proof state:
case h
p : Pos
c₁ c₂ : Char
⊢ p.byteIdx + c₁.utf8Size + c₂.utf8Size = p.byteIdx + c₂.utf8Size + c₁.utf8Size

Tactic:
apply Nat.add_right_comm

Result:
no goals

Proof state:
case h
p : Pos
c₁ c₂ : Char
⊢ p.byteIdx + c₁.utf8Size + c₂.utf8Size = (p + c₂).byteIdx + c₁.utf8Size

Tactic:
rw [pos_add_char]

Result:
case h
p : Pos
c₁ c₂ : Char
⊢ p.byteIdx + c₁.utf8Size + c₂.utf8Size = p.byteIdx + c₂.utf8Size + c₁.utf8Size

Proof state:
case h
p : Pos
c₁ c₂ : Char
⊢ (p + c₁ + c₂).byteIdx = (p + c₂ + c₁).byteIdx

Tactic:
repeat rw [pos_add_char]

Result:
case h
p : Pos
c₁ c₂ : Char
⊢ p.byteIdx + c₁.utf8Size + c₂.utf8Size = p.byteIdx + c₂.utf8Size + c₁.utf8Size
-- Mathlib/CategoryTheory/Filtered/Basic.lean
theorem coeq₃_condition₁ {j₁ j₂ : C} (f g h : j₁ ⟶ j₂) :
    f ≫ coeq₃Hom f g h = g ≫ coeq₃Hom f g h

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : IsFilteredOrEmpty C
j₁ j₂ : C
f g h : j₁ ⟶ j₂
⊢ f ≫ coeq₃Hom f g h = g ≫ coeq₃Hom f g h

Tactic:
simp only [coeq₃Hom, ← Category.assoc, coeq_condition f g]

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Basic.lean
theorem lift_mk_shrink'' (α : Type max u v) [Small.{v} α] :
    Cardinal.lift.{u} #(Shrink.{v} α) = #α

Proof state:
α : Type (max u v)
inst✝ : Small.{v, max u v} α
⊢ lift.{u, v} #(Shrink.{v, max u v} α) = #α

Tactic:
rw [← lift_umax, lift_mk_shrink.{max u v, v, 0} α, ← lift_umax, lift_id]

Result:
no goals
-- Mathlib/Topology/Algebra/InfiniteSum/Basic.lean
theorem tprod_one : ∏' _ : β, (1 : α) = 1

Proof state:
α : Type u_1
β : Type u_2
inst✝¹ : CommMonoid α
inst✝ : TopologicalSpace α
⊢ ∏' (x : β), 1 = 1

Tactic:
rw [tprod_eq_finprod] <;> simp

Result:
no goals
-- Mathlib/Data/Matroid/Constructions.lean
theorem uniqueBaseOn_inter_isBasis (hX : X ⊆ E) : (uniqueBaseOn I E).IsBasis (X ∩ I) X

Proof state:
α : Type u_1
E I X : Set α
hX : X ⊆ E
⊢ (uniqueBaseOn I E).IsBasis (X ∩ I) X

Tactic:
rw [uniqueBaseOn_isBasis_iff hX]

Result:
no goals
-- Mathlib/Data/Complex/Trigonometric.lean
theorem norm_cos_add_sin_mul_I (x : ℝ) : ‖cos x + sin x * I‖ = 1

Proof state:
x : ℝ
this : Real.sin x ^ 2 + Real.cos x ^ 2 = 1
⊢ ‖cos ↑x + sin ↑x * I‖ = 1

Tactic:
simp_all [add_comm, norm_def, normSq, sq, sin_ofReal_re, cos_ofReal_re, mul_re]

Result:
no goals

Proof state:
x : ℝ
⊢ ‖cos ↑x + sin ↑x * I‖ = 1

Tactic:
have := Real.sin_sq_add_cos_sq x

Result:
x : ℝ
this : Real.sin x ^ 2 + Real.cos x ^ 2 = 1
⊢ ‖cos ↑x + sin ↑x * I‖ = 1
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Find.lean
theorem get_find?_mem {xs : Array α} (h) : (xs.find? p).get h ∈ xs

Proof state:
α : Type u_1
p : α → Bool
xs : Array α
h : (find? p xs).isSome = true
⊢ (find? p xs).get h ∈ xs

Tactic:
cases xs

Result:
case mk
α : Type u_1
p : α → Bool
toList✝ : List α
h : (find? p { toList := toList✝ }).isSome = true
⊢ (find? p { toList := toList✝ }).get h ∈ { toList := toList✝ }

Proof state:
case mk
α : Type u_1
p : α → Bool
toList✝ : List α
h : (find? p { toList := toList✝ }).isSome = true
⊢ (find? p { toList := toList✝ }).get h ∈ { toList := toList✝ }

Tactic:
simp [List.get_find?_mem]

Result:
no goals
-- Mathlib/RingTheory/GradedAlgebra/Basic.lean
theorem coe_decompose_mul_of_right_mem (n) [Decidable (i ≤ n)] (b_mem : b ∈ 𝒜 i) :
    (decompose 𝒜 (a * b) n : A) = if i ≤ n then decompose 𝒜 a (n - i) * b else 0

Proof state:
case intro
ι : Type u_1
A : Type u_3
σ : Type u_4
inst✝¹¹ : Semiring A
inst✝¹⁰ : DecidableEq ι
inst✝⁹ : AddCommMonoid ι
inst✝⁸ : PartialOrder ι
inst✝⁷ : CanonicallyOrderedAdd ι
inst✝⁶ : SetLike σ A
inst✝⁵ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝⁴ : GradedRing 𝒜
a : A
i : ι
inst✝³ : Sub ι
inst✝² : OrderedSub ι
inst✝¹ : AddLeftReflectLE ι
n : ι
inst✝ : Decidable (i ≤ n)
b : ↥(𝒜 i)
⊢ ↑(((decompose 𝒜) (a * ↑b)) n) = if i ≤ n then ↑(((decompose 𝒜) a) (n - i)) * ↑b else 0

Tactic:
rw [decompose_mul, decompose_coe, coe_mul_of_apply]

Result:
no goals

Proof state:
ι : Type u_1
A : Type u_3
σ : Type u_4
inst✝¹¹ : Semiring A
inst✝¹⁰ : DecidableEq ι
inst✝⁹ : AddCommMonoid ι
inst✝⁸ : PartialOrder ι
inst✝⁷ : CanonicallyOrderedAdd ι
inst✝⁶ : SetLike σ A
inst✝⁵ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝⁴ : GradedRing 𝒜
a b : A
i : ι
inst✝³ : Sub ι
inst✝² : OrderedSub ι
inst✝¹ : AddLeftReflectLE ι
n : ι
inst✝ : Decidable (i ≤ n)
b_mem : b ∈ 𝒜 i
⊢ ↑(((decompose 𝒜) (a * b)) n) = if i ≤ n then ↑(((decompose 𝒜) a) (n - i)) * b else 0

Tactic:
lift b to 𝒜 i using b_mem

Result:
case intro
ι : Type u_1
A : Type u_3
σ : Type u_4
inst✝¹¹ : Semiring A
inst✝¹⁰ : DecidableEq ι
inst✝⁹ : AddCommMonoid ι
inst✝⁸ : PartialOrder ι
inst✝⁷ : CanonicallyOrderedAdd ι
inst✝⁶ : SetLike σ A
inst✝⁵ : AddSubmonoidClass σ A
𝒜 : ι → σ
inst✝⁴ : GradedRing 𝒜
a : A
i : ι
inst✝³ : Sub ι
inst✝² : OrderedSub ι
inst✝¹ : AddLeftReflectLE ι
n : ι
inst✝ : Decidable (i ≤ n)
b : ↥(𝒜 i)
⊢ ↑(((decompose 𝒜) (a * ↑b)) n) = if i ≤ n then ↑(((decompose 𝒜) a) (n - i)) * ↑b else 0
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem nil_eq_append_iff : [] = a ++ b ↔ a = [] ∧ b = []

Proof state:
α✝ : Type u_1
a b : List α✝
⊢ [] = a ++ b ↔ a = [] ∧ b = []

Tactic:
rw [eq_comm, append_eq_nil_iff]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Triangle/Tripartite.lean
@[simp] lemma in₂₀_iff : (graph t).Adj (in₂ c) (in₀ a) ↔ ∃ b, (a, b, c) ∈ t :=
  ⟨by rintro ⟨⟩; exact ⟨_, ‹_›⟩, fun ⟨_, h⟩ ↦ in₂₀ h⟩

Proof state:
case in₂₀
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
a : α
c : γ
b✝ : β
a✝ : (a, b✝, c) ∈ t
⊢ ∃ b, (a, b, c) ∈ t

Tactic:
exact ⟨_, ‹_›⟩

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
a : α
c : γ
⊢ (graph t).Adj (in₂ c) (in₀ a) → ∃ b, (a, b, c) ∈ t

Tactic:
rintro ⟨⟩

Result:
case in₂₀
α : Type u_1
β : Type u_2
γ : Type u_3
t : Finset (α × β × γ)
a : α
c : γ
b✝ : β
a✝ : (a, b✝, c) ∈ t
⊢ ∃ b, (a, b, c) ∈ t
-- Mathlib/Algebra/MvPolynomial/Variables.lean
theorem vars_sum_of_disjoint [DecidableEq σ] (h : Pairwise <| (Disjoint on fun i => (φ i).vars)) :
    (∑ i ∈ t, φ i).vars = Finset.biUnion t fun i => (φ i).vars

Proof state:
case insert
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
ι : Type u_3
t : Finset ι
φ : ι → MvPolynomial σ R
inst✝ : DecidableEq σ
h : Pairwise (Disjoint on fun i => (φ i).vars)
a✝ : ι
s✝ : Finset ι
has : a✝ ∉ s✝
hsum : (∑ i ∈ s✝, φ i).vars = s✝.biUnion fun i => (φ i).vars
⊢ Disjoint (φ a✝).vars (∑ x ∈ s✝, φ x).vars

Tactic:
unfold Pairwise onFun at h

Result:
case insert
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
ι : Type u_3
t : Finset ι
φ : ι → MvPolynomial σ R
inst✝ : DecidableEq σ
h : ∀ ⦃i j : ι⦄, i ≠ j → Disjoint ((fun i => (φ i).vars) i) ((fun i => (φ i).vars) j)
a✝ : ι
s✝ : Finset ι
has : a✝ ∉ s✝
hsum : (∑ i ∈ s✝, φ i).vars = s✝.biUnion fun i => (φ i).vars
⊢ Disjoint (φ a✝).vars (∑ x ∈ s✝, φ x).vars

Proof state:
case insert
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
ι : Type u_3
t : Finset ι
φ : ι → MvPolynomial σ R
inst✝ : DecidableEq σ
h : ∀ ⦃i j : ι⦄, i ≠ j → Disjoint ((fun i => (φ i).vars) i) ((fun i => (φ i).vars) j)
a✝ : ι
s✝ : Finset ι
has : a✝ ∉ s✝
hsum : (∑ i ∈ s✝, φ i).vars = s✝.biUnion fun i => (φ i).vars
⊢ Disjoint (φ a✝).vars (s✝.biUnion fun i => (φ i).vars)

Tactic:
simp only [Finset.disjoint_iff_ne] at h ⊢

Result:
case insert
R : Type u
σ : Type u_1
inst✝¹ : CommSemiring R
ι : Type u_3
t : Finset ι
φ : ι → MvPolynomial σ R
inst✝ : DecidableEq σ
a✝ : ι
s✝ : Finset ι
has : a✝ ∉ s✝
hsum : (∑ i ∈ s✝, φ i).vars = s✝.biUnion fun i => (φ i).vars
h : ∀ ⦃i j : ι⦄, i ≠ j → ∀ a ∈ (φ i).vars, ∀ b ∈ (φ j).vars, a ≠ b
⊢ ∀ a ∈ (φ a✝).vars, ∀ b ∈ s✝.biUnion fun i => (φ i).vars, a ≠ b
-- Mathlib/Data/DFinsupp/Interval.lean
lemma card_Ioo : #(Ioo f g) = (∏ i ∈ f.support ∪ g.support, #(Icc (f i) (g i))) - 2

Proof state:
ι : Type u_1
α : ι → Type u_2
inst✝⁴ : DecidableEq ι
inst✝³ : (i : ι) → DecidableEq (α i)
inst✝² : (i : ι) → PartialOrder (α i)
inst✝¹ : (i : ι) → Zero (α i)
inst✝ : (i : ι) → LocallyFiniteOrder (α i)
f g : Π₀ (i : ι), α i
⊢ #(Ioo f g) = ∏ i ∈ f.support ∪ g.support, #(Icc (f i) (g i)) - 2

Tactic:
rw [card_Ioo_eq_card_Icc_sub_two, card_Icc]

Result:
no goals
-- Mathlib/Order/SuccPred/Basic.lean
lemma not_succ_mem_iff_isMax [SuccOrder α] [NoMaxOrder α] {a : s} :
    succ ↑a ∉ s ↔ IsMax a where
  mp := isMax_of_not_succ_mem
  mpr h nh

Proof state:
α : Type u_3
inst✝³ : PartialOrder α
s : Set α
inst✝² : s.OrdConnected
inst✝¹ : SuccOrder α
inst✝ : NoMaxOrder α
a : ↑s
h : IsMax a
nh : succ ↑a ∈ s
⊢ False

Tactic:
replace h := congr($h.succ_eq.1)

Result:
α : Type u_3
inst✝³ : PartialOrder α
s : Set α
inst✝² : s.OrdConnected
inst✝¹ : SuccOrder α
inst✝ : NoMaxOrder α
a : ↑s
nh : succ ↑a ∈ s
h : ↑(succ a) = ↑a
⊢ False

Proof state:
α : Type u_3
inst✝³ : PartialOrder α
s : Set α
inst✝² : s.OrdConnected
inst✝¹ : SuccOrder α
inst✝ : NoMaxOrder α
a : ↑s
nh : succ ↑a ∈ s
h : succ ↑a = ↑a
⊢ False

Tactic:
simp at h

Result:
no goals

Proof state:
α : Type u_3
inst✝³ : PartialOrder α
s : Set α
inst✝² : s.OrdConnected
inst✝¹ : SuccOrder α
inst✝ : NoMaxOrder α
a : ↑s
nh : succ ↑a ∈ s
h : ↑(succ a) = ↑a
⊢ False

Tactic:
rw [coe_succ_of_mem nh] at h

Result:
α : Type u_3
inst✝³ : PartialOrder α
s : Set α
inst✝² : s.OrdConnected
inst✝¹ : SuccOrder α
inst✝ : NoMaxOrder α
a : ↑s
nh : succ ↑a ∈ s
h : succ ↑a = ↑a
⊢ False
-- Mathlib/CategoryTheory/Monoidal/Preadditive.lean
theorem zero_tensor {W X Y Z : C} (f : Y ⟶ Z) : (0 : W ⟶ X) ⊗ f = 0

Proof state:
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : Preadditive C
inst✝¹ : MonoidalCategory C
inst✝ : MonoidalPreadditive C
W X Y Z : C
f : Y ⟶ Z
⊢ 0 ⊗ f = 0

Tactic:
simp [tensorHom_def]

Result:
no goals
-- Mathlib/Probability/Kernel/Condexp.lean
lemma condExpKernel_ae_eq_trim_condExp
    (hm : m ≤ mΩ) {s : Set Ω} (hs : MeasurableSet s) :
    (fun ω ↦ (condExpKernel μ m ω s).toReal) =ᵐ[μ.trim hm] μ⟦s | m⟧

Proof state:
Ω : Type u_1
m mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hm : m ≤ mΩ
s : Set Ω
hs : MeasurableSet s
⊢ (fun x => (((condExpKernel μ m) x) s).toReal) =ᶠ[ae μ] μ[s.indicator fun ω => 1|m]

Tactic:
exact condExpKernel_ae_eq_condExp hm hs

Result:
no goals

Proof state:
Ω : Type u_1
m mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hm : m ≤ mΩ
s : Set Ω
hs : MeasurableSet s
⊢ (fun ω => (((condExpKernel μ m) ω) s).toReal) =ᶠ[ae (μ.trim hm)] μ[s.indicator fun ω => 1|m]

Tactic:
rw [(measurable_condExpKernel hs).ennreal_toReal.stronglyMeasurable.ae_eq_trim_iff hm
  stronglyMeasurable_condExp]

Result:
Ω : Type u_1
m mΩ : MeasurableSpace Ω
inst✝¹ : StandardBorelSpace Ω
μ : Measure Ω
inst✝ : IsFiniteMeasure μ
hm : m ≤ mΩ
s : Set Ω
hs : MeasurableSet s
⊢ (fun x => (((condExpKernel μ m) x) s).toReal) =ᶠ[ae μ] μ[s.indicator fun ω => 1|m]
-- Mathlib/Algebra/Order/ToIntervalMod.lean
theorem iUnion_Ico_zsmul : ⋃ n : ℤ, Ico (n • p) ((n + 1) • p) = univ

Proof state:
α : Type u_1
inst✝¹ : LinearOrderedAddCommGroup α
inst✝ : Archimedean α
p : α
hp : 0 < p
⊢ ⋃ n, Ico (n • p) ((n + 1) • p) = univ

Tactic:
simpa only [zero_add] using iUnion_Ico_add_zsmul hp 0

Result:
no goals
-- Mathlib/MeasureTheory/Integral/IntervalIntegral.lean
theorem integral_comp_add_div (hc : c ≠ 0) (d) :
    (∫ x in a..b, f (d + x / c)) = c • ∫ x in d + a / c..d + b / c, f x

Proof state:
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
a b c : ℝ
f : ℝ → E
hc : c ≠ 0
d : ℝ
⊢ ∫ (x : ℝ) in a..b, f (d + x / c) = c • ∫ (x : ℝ) in d + a / c..d + b / c, f x

Tactic:
simpa only [div_eq_inv_mul, inv_inv] using integral_comp_add_mul f (inv_ne_zero hc) d

Result:
no goals
-- Mathlib/Data/Real/Basic.lean
theorem cauchy_inv : ∀ f, (f⁻¹ : ℝ).cauchy = f.cauchy⁻¹
  | ⟨f⟩ => show (inv' _).cauchy = _ by rw [inv']

Proof state:
f : Cauchy abs
⊢ (Real.inv' { cauchy := f }).cauchy = { cauchy := f }.cauchy⁻¹

Tactic:
rw [inv']

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/PropLemmas.lean
theorem Decidable.not_iff_not [Decidable a] [Decidable b] : (¬a ↔ ¬b) ↔ (a ↔ b)

Proof state:
a b : Prop
inst✝¹ : Decidable a
inst✝ : Decidable b
⊢ (¬a ↔ ¬b) ↔ (a ↔ b)

Tactic:
rw [@iff_def (¬a), @iff_def' a]

Result:
a b : Prop
inst✝¹ : Decidable a
inst✝ : Decidable b
⊢ (¬a → ¬b) ∧ (¬b → ¬a) ↔ (b → a) ∧ (a → b)

Proof state:
a b : Prop
inst✝¹ : Decidable a
inst✝ : Decidable b
⊢ (¬a → ¬b) ∧ (¬b → ¬a) ↔ (b → a) ∧ (a → b)

Tactic:
exact and_congr not_imp_not not_imp_not

Result:
no goals
-- Mathlib/LinearAlgebra/Dimension/Free.lean
theorem finrank_of_not_finite (h : ¬Module.Finite R M) : finrank R M = 0

Proof state:
R : Type u
M : Type v
inst✝⁴ : Semiring R
inst✝³ : StrongRankCondition R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Free R M
h : ¬Module.Finite R M
⊢ Module.rank R M = 0 ∨ ¬Module.Finite R M

Tactic:
exact .inr h

Result:
no goals

Proof state:
R : Type u
M : Type v
inst✝⁴ : Semiring R
inst✝³ : StrongRankCondition R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Free R M
h : ¬Module.Finite R M
⊢ finrank R M = 0

Tactic:
rw [finrank, toNat_eq_zero, ← not_lt, Module.rank_lt_aleph0_iff]

Result:
R : Type u
M : Type v
inst✝⁴ : Semiring R
inst✝³ : StrongRankCondition R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
inst✝ : Free R M
h : ¬Module.Finite R M
⊢ Module.rank R M = 0 ∨ ¬Module.Finite R M
-- Mathlib/AlgebraicGeometry/OpenImmersion.lean
@[reassoc (attr := simp)]
lemma appIso_inv_appLE {X Y : Scheme.{u}} (f : X ⟶ Y) [IsOpenImmersion f] {U V : X.Opens}
    (e : V ≤ f ⁻¹ᵁ f ''ᵁ U) :
    (f.appIso U).inv ≫ f.appLE (f ''ᵁ U) V e =
        X.presheaf.map (homOfLE (by rwa [preimage_image_eq] at e)).op

Proof state:
X Y : Scheme
f : X ⟶ Y
inst✝ : IsOpenImmersion f
U V : X.Opens
e : V ≤ f ⁻¹ᵁ f ''ᵁ U
⊢ X.presheaf.map (eqToHom ⋯ ≫ (homOfLE e).op) = X.presheaf.map (homOfLE ⋯).op

Tactic:
rfl

Result:
no goals

Proof state:
X Y : Scheme
f : X ⟶ Y
inst✝ : IsOpenImmersion f
U V : X.Opens
e : V ≤ f ⁻¹ᵁ f ''ᵁ U
⊢ (appIso f U).inv ≫ appLE f (f ''ᵁ U) V e = X.presheaf.map (homOfLE ⋯).op

Tactic:
simp only [appLE, appIso_inv_app_assoc, eqToHom_op]

Result:
X Y : Scheme
f : X ⟶ Y
inst✝ : IsOpenImmersion f
U V : X.Opens
e : V ≤ f ⁻¹ᵁ f ''ᵁ U
⊢ X.presheaf.map (eqToHom ⋯) ≫ X.presheaf.map (homOfLE e).op = X.presheaf.map (homOfLE ⋯).op

Proof state:
X Y : Scheme
f : X ⟶ Y
inst✝ : IsOpenImmersion f
U V : X.Opens
e : V ≤ f ⁻¹ᵁ f ''ᵁ U
⊢ X.presheaf.map (eqToHom ⋯) ≫ X.presheaf.map (homOfLE e).op = X.presheaf.map (homOfLE ⋯).op

Tactic:
rw [← Functor.map_comp]

Result:
X Y : Scheme
f : X ⟶ Y
inst✝ : IsOpenImmersion f
U V : X.Opens
e : V ≤ f ⁻¹ᵁ f ''ᵁ U
⊢ X.presheaf.map (eqToHom ⋯ ≫ (homOfLE e).op) = X.presheaf.map (homOfLE ⋯).op

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
X✝ Y✝ : Scheme
f✝ : X✝.Hom Y✝
H : IsOpenImmersion f✝
X Y : Scheme
f : X ⟶ Y
inst✝ : IsOpenImmersion f
U V : X.Opens
e : V ≤ f ⁻¹ᵁ f ''ᵁ U
⊢ V ≤ U

Tactic:
rwa [preimage_image_eq] at e

Result:
no goals
-- Mathlib/Algebra/Polynomial/Degree/Domain.lean
/-- This lemma is useful for working with the `intDegree` of a rational function. -/
lemma natDegree_sub_eq_of_prod_eq {p₁ p₂ q₁ q₂ : R[X]} (hp₁ : p₁ ≠ 0) (hq₁ : q₁ ≠ 0)
    (hp₂ : p₂ ≠ 0) (hq₂ : q₂ ≠ 0) (h_eq : p₁ * q₂ = p₂ * q₁) :
    (p₁.natDegree : ℤ) - q₁.natDegree = (p₂.natDegree : ℤ) - q₂.natDegree

Proof state:
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p₁ p₂ q₁ q₂ : R[X]
hp₁ : p₁ ≠ 0
hq₁ : q₁ ≠ 0
hp₂ : p₂ ≠ 0
hq₂ : q₂ ≠ 0
h_eq : p₁ * q₂ = p₂ * q₁
⊢ ↑p₁.natDegree - ↑q₁.natDegree = ↑p₂.natDegree - ↑q₂.natDegree

Tactic:
rw [sub_eq_sub_iff_add_eq_add]

Result:
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p₁ p₂ q₁ q₂ : R[X]
hp₁ : p₁ ≠ 0
hq₁ : q₁ ≠ 0
hp₂ : p₂ ≠ 0
hq₂ : q₂ ≠ 0
h_eq : p₁ * q₂ = p₂ * q₁
⊢ ↑p₁.natDegree + ↑q₂.natDegree = ↑p₂.natDegree + ↑q₁.natDegree

Proof state:
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p₁ p₂ q₁ q₂ : R[X]
hp₁ : p₁ ≠ 0
hq₁ : q₁ ≠ 0
hp₂ : p₂ ≠ 0
hq₂ : q₂ ≠ 0
h_eq : p₁ * q₂ = p₂ * q₁
⊢ ↑p₁.natDegree + ↑q₂.natDegree = ↑p₂.natDegree + ↑q₁.natDegree

Tactic:
norm_cast

Result:
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p₁ p₂ q₁ q₂ : R[X]
hp₁ : p₁ ≠ 0
hq₁ : q₁ ≠ 0
hp₂ : p₂ ≠ 0
hq₂ : q₂ ≠ 0
h_eq : p₁ * q₂ = p₂ * q₁
⊢ p₁.natDegree + q₂.natDegree = p₂.natDegree + q₁.natDegree

Proof state:
R : Type u
inst✝¹ : Semiring R
inst✝ : NoZeroDivisors R
p₁ p₂ q₁ q₂ : R[X]
hp₁ : p₁ ≠ 0
hq₁ : q₁ ≠ 0
hp₂ : p₂ ≠ 0
hq₂ : q₂ ≠ 0
h_eq : p₁ * q₂ = p₂ * q₁
⊢ p₁.natDegree + q₂.natDegree = p₂.natDegree + q₁.natDegree

Tactic:
rw [← natDegree_mul hp₁ hq₂, ← natDegree_mul hp₂ hq₁, h_eq]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Order.lean
theorem lt_add_of_pos_left (a : Int) {b : Int} (h : 0 < b) : a < b + a

Proof state:
a b : Int
h : 0 < b
⊢ a < b + a

Tactic:
have : 0 + a < b + a := Int.add_lt_add_right h a

Result:
a b : Int
h : 0 < b
this : 0 + a < b + a
⊢ a < b + a

Proof state:
a b : Int
h : 0 < b
this : 0 + a < b + a
⊢ a < b + a

Tactic:
rwa [Int.zero_add] at this

Result:
no goals
-- Mathlib/Topology/Bornology/Absorbs.lean
theorem absorbs_finite (hs : Absorbent M s) (ht : t.Finite) : Absorbs M s t

Proof state:
M : Type u_1
α : Type u_2
inst✝¹ : Bornology M
inst✝ : SMul M α
s t : Set α
hs : Absorbent M s
ht : t.Finite
⊢ Absorbs M s (⋃ x ∈ t, {x})

Tactic:
exact .biUnion ht fun _ _ => hs.absorbs

Result:
no goals

Proof state:
M : Type u_1
α : Type u_2
inst✝¹ : Bornology M
inst✝ : SMul M α
s t : Set α
hs : Absorbent M s
ht : t.Finite
⊢ Absorbs M s t

Tactic:
rw [← Set.biUnion_of_singleton t]

Result:
M : Type u_1
α : Type u_2
inst✝¹ : Bornology M
inst✝ : SMul M α
s t : Set α
hs : Absorbent M s
ht : t.Finite
⊢ Absorbs M s (⋃ x ∈ t, {x})