harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/NumberTheory/Cyclotomic/CyclotomicCharacter.lean
lemma unique (g : L ≃+* L) {c : ZMod n} (hc : ∀ t ∈ rootsOfUnity n L, g t = t ^ c.val) :
    c = ModularCyclotomicCharacter L hn g

Proof state:
L : Type u
inst✝² : CommRing L
inst✝¹ : IsDomain L
n : ℕ
inst✝ : NeZero n
hn : Fintype.card ↥(rootsOfUnity n L) = n
g : L ≃+* L
c : ZMod n
hc : ∀ t ∈ rootsOfUnity n L, g ↑t = ↑t ^ c.val
t : Lˣ
ht : t ∈ rootsOfUnity n L
⊢ g ↑t = ↑t ^ ((ZMod.ringEquivCongr ⋯) c).val

Tactic:
rw [hc t ht, ZMod.ringEquivCongr_val]

Result:
no goals

Proof state:
L : Type u
inst✝² : CommRing L
inst✝¹ : IsDomain L
n : ℕ
inst✝ : NeZero n
hn : Fintype.card ↥(rootsOfUnity n L) = n
g : L ≃+* L
c : ZMod n
hc : ∀ t ∈ rootsOfUnity n L, g ↑t = ↑t ^ c.val
⊢ c = ↑((ModularCyclotomicCharacter L hn) g)

Tactic:
change c = (ZMod.ringEquivCongr hn) (toFun n g)

Result:
L : Type u
inst✝² : CommRing L
inst✝¹ : IsDomain L
n : ℕ
inst✝ : NeZero n
hn : Fintype.card ↥(rootsOfUnity n L) = n
g : L ≃+* L
c : ZMod n
hc : ∀ t ∈ rootsOfUnity n L, g ↑t = ↑t ^ c.val
⊢ c = (ZMod.ringEquivCongr hn) (toFun n g)

Proof state:
L : Type u
inst✝² : CommRing L
inst✝¹ : IsDomain L
n : ℕ
inst✝ : NeZero n
hn : Fintype.card ↥(rootsOfUnity n L) = n
g : L ≃+* L
c : ZMod n
hc : ∀ t ∈ rootsOfUnity n L, g ↑t = ↑t ^ c.val
⊢ c = (ZMod.ringEquivCongr hn) (toFun n g)

Tactic:
rw [← toFun_unique' n g (ZMod.ringEquivCongr hn.symm c)
  (fun t ht ↦ by rw [hc t ht, ZMod.ringEquivCongr_val]), ← ZMod.ringEquivCongr_symm hn,
  RingEquiv.apply_symm_apply]

Result:
no goals
-- Mathlib/Order/Interval/Set/Basic.lean
theorem Ico_eq_empty_iff : Ico a b = ∅ ↔ ¬a < b

Proof state:
α : Type u_1
inst✝ : Preorder α
a b : α
⊢ Ico a b = ∅ ↔ ¬a < b

Tactic:
rw [← not_nonempty_iff_eq_empty, not_iff_not, nonempty_Ico]

Result:
no goals
-- Mathlib/MeasureTheory/Decomposition/Jordan.lean
theorem real_smul_negPart_neg (r : ℝ) (hr : r < 0) :
    (r • j).negPart = (-r).toNNReal • j.posPart

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
j : JordanDecomposition α
r : ℝ
hr : r < 0
⊢ (r • j).negPart = (-r).toNNReal • j.posPart

Tactic:
rw [real_smul_def, ← smul_posPart, if_neg (not_le.2 hr), neg_negPart]

Result:
no goals
-- Mathlib/CategoryTheory/Subobject/Basic.lean
theorem ofMkLE_comp_ofLE {B A₁ : C} (f : A₁ ⟶ B) [Mono f] (X Y : Subobject B) (h₁ : mk f ≤ X)
    (h₂ : X ≤ Y) : ofMkLE f X h₁ ≫ ofLE X Y h₂ = ofMkLE f Y (h₁.trans h₂)

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
B A₁ : C
f : A₁ ⟶ B
inst✝ : Mono f
X Y : Subobject B
h₁ : mk f ≤ X
h₂ : X ≤ Y
⊢ ofMkLE f X h₁ ≫ X.ofLE Y h₂ = ofMkLE f Y ⋯

Tactic:
simp only [ofMkLE, ofLEMk, ofLE, ofMkLEMk, ← Functor.map_comp underlying,
  assoc]

Result:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
B A₁ : C
f : A₁ ⟶ B
inst✝ : Mono f
X Y : Subobject B
h₁ : mk f ≤ X
h₂ : X ≤ Y
⊢ (underlyingIso f).inv ≫ underlying.map (h₁.hom ≫ h₂.hom) = (underlyingIso f).inv ≫ underlying.map ⋯.hom

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
B A₁ : C
f : A₁ ⟶ B
inst✝ : Mono f
X Y : Subobject B
h₁ : mk f ≤ X
h₂ : X ≤ Y
⊢ (underlyingIso f).inv ≫ underlying.map (h₁.hom ≫ h₂.hom) = (underlyingIso f).inv ≫ underlying.map ⋯.hom

Tactic:
congr 1

Result:
no goals
-- Mathlib/Order/Filter/AtTopBot/Basic.lean
theorem map_sub_atTop_eq_nat (k : ℕ) : map (fun a => a - k) atTop = atTop :=
  map_atTop_eq_of_gc (· + k) 0 (fun _ _ h => Nat.sub_le_sub_right h _)
    (fun _ _ _ => Nat.sub_le_iff_le_add) fun b _ => by rw [Nat.add_sub_cancel_right]

Proof state:
k b : ℕ
x✝ : b ≥ 0
⊢ b ≤ (fun x => x + k) b - k

Tactic:
rw [Nat.add_sub_cancel_right]

Result:
no goals
-- Mathlib/Data/Finset/NAry.lean
theorem image₂_distrib_subset_left {γ : Type*} {u : Finset γ} {f : α → δ → ε} {g : β → γ → δ}
    {f₁ : α → β → β'} {f₂ : α → γ → γ'} {g' : β' → γ' → ε}
    (h_distrib : ∀ a b c, f a (g b c) = g' (f₁ a b) (f₂ a c)) :
    image₂ f s (image₂ g t u) ⊆ image₂ g' (image₂ f₁ s t) (image₂ f₂ s u) :=
  coe_subset.1 <| by
    push_cast
    exact Set.image2_distrib_subset_left h_distrib

Proof state:
α : Type u_1
β : Type u_3
β' : Type u_4
γ' : Type u_6
δ : Type u_7
ε : Type u_9
inst✝³ : DecidableEq β'
inst✝² : DecidableEq γ'
inst✝¹ : DecidableEq ε
s : Finset α
t : Finset β
inst✝ : DecidableEq δ
γ : Type u_14
u : Finset γ
f : α → δ → ε
g : β → γ → δ
f₁ : α → β → β'
f₂ : α → γ → γ'
g' : β' → γ' → ε
h_distrib : ∀ (a : α) (b : β) (c : γ), f a (g b c) = g' (f₁ a b) (f₂ a c)
⊢ ↑(image₂ f s (image₂ g t u)) ⊆ ↑(image₂ g' (image₂ f₁ s t) (image₂ f₂ s u))

Tactic:
push_cast

Result:
α : Type u_1
β : Type u_3
β' : Type u_4
γ' : Type u_6
δ : Type u_7
ε : Type u_9
inst✝³ : DecidableEq β'
inst✝² : DecidableEq γ'
inst✝¹ : DecidableEq ε
s : Finset α
t : Finset β
inst✝ : DecidableEq δ
γ : Type u_14
u : Finset γ
f : α → δ → ε
g : β → γ → δ
f₁ : α → β → β'
f₂ : α → γ → γ'
g' : β' → γ' → ε
h_distrib : ∀ (a : α) (b : β) (c : γ), f a (g b c) = g' (f₁ a b) (f₂ a c)
⊢ image2 f (↑s) (image2 g ↑t ↑u) ⊆ image2 g' (image2 f₁ ↑s ↑t) (image2 f₂ ↑s ↑u)

Proof state:
α : Type u_1
β : Type u_3
β' : Type u_4
γ' : Type u_6
δ : Type u_7
ε : Type u_9
inst✝³ : DecidableEq β'
inst✝² : DecidableEq γ'
inst✝¹ : DecidableEq ε
s : Finset α
t : Finset β
inst✝ : DecidableEq δ
γ : Type u_14
u : Finset γ
f : α → δ → ε
g : β → γ → δ
f₁ : α → β → β'
f₂ : α → γ → γ'
g' : β' → γ' → ε
h_distrib : ∀ (a : α) (b : β) (c : γ), f a (g b c) = g' (f₁ a b) (f₂ a c)
⊢ image2 f (↑s) (image2 g ↑t ↑u) ⊆ image2 g' (image2 f₁ ↑s ↑t) (image2 f₂ ↑s ↑u)

Tactic:
exact Set.image2_distrib_subset_left h_distrib

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem getEntry?_eq_some_getEntry [BEq α] {l : List ((a : α) × β a)} {a : α}
    (h : containsKey a l) : getEntry? a l = some (getEntry a l h)

Proof state:
α : Type u
β : α → Type v
inst✝ : BEq α
l : List ((a : α) × β a)
a : α
h : containsKey a l = true
⊢ getEntry? a l = some (getEntry a l h)

Tactic:
simp [getEntry]

Result:
no goals
-- Mathlib/Analysis/Calculus/ContDiff/Operations.lean
theorem ContDiffAt.sub {f g : E → F} (hf : ContDiffAt 𝕜 n f x) (hg : ContDiffAt 𝕜 n g x) :
    ContDiffAt 𝕜 n (fun x => f x - g x) x

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
x : E
n : WithTop ℕ∞
f g : E → F
hf : ContDiffAt 𝕜 n f x
hg : ContDiffAt 𝕜 n g x
⊢ ContDiffAt 𝕜 n (fun x => f x - g x) x

Tactic:
simpa only [sub_eq_add_neg] using hf.add hg.neg

Result:
no goals
-- Mathlib/MeasureTheory/Integral/CircleIntegral.lean
theorem norm_integral_le_of_norm_le_const {f : ℂ → E} {c : ℂ} {R C : ℝ} (hR : 0 ≤ R)
    (hf : ∀ z ∈ sphere c R, ‖f z‖ ≤ C) : ‖∮ z in C(c, R), f z‖ ≤ 2 * π * R * C :=
  have : |R| = R := abs_of_nonneg hR
  calc
    ‖∮ z in C(c, R), f z‖ ≤ 2 * π * |R| * C := norm_integral_le_of_norm_le_const' <| by rwa [this]
    _ = 2 * π * R * C

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
c : ℂ
R C : ℝ
hR : 0 ≤ R
hf : ∀ z ∈ sphere c R, ‖f z‖ ≤ C
this : |R| = R
⊢ 2 * π * |R| * C = 2 * π * R * C

Tactic:
rw [this]

Result:
no goals

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f : ℂ → E
c : ℂ
R C : ℝ
hR : 0 ≤ R
hf : ∀ z ∈ sphere c R, ‖f z‖ ≤ C
this : |R| = R
⊢ ∀ z ∈ sphere c |R|, ‖f z‖ ≤ C

Tactic:
rwa [this]

Result:
no goals
-- Mathlib/Order/Ideal.lean
theorem eq_sup_of_le_sup {x i j : P} (hi : i ∈ I) (hj : j ∈ J) (hx : x ≤ i ⊔ j) :
    ∃ i' ∈ I, ∃ j' ∈ J, x = i' ⊔ j'

Proof state:
P : Type u_1
inst✝ : DistribLattice P
I J : Ideal P
x i j : P
hi : i ∈ I
hj : j ∈ J
hx : x ≤ i ⊔ j
⊢ ∃ i' ∈ I, ∃ j' ∈ J, x = i' ⊔ j'

Tactic:
refine ⟨x ⊓ i, I.lower inf_le_right hi, x ⊓ j, J.lower inf_le_right hj, ?_⟩

Result:
P : Type u_1
inst✝ : DistribLattice P
I J : Ideal P
x i j : P
hi : i ∈ I
hj : j ∈ J
hx : x ≤ i ⊔ j
⊢ x = x ⊓ i ⊔ x ⊓ j

Proof state:
P : Type u_1
inst✝ : DistribLattice P
I J : Ideal P
x i j : P
hi : i ∈ I
hj : j ∈ J
hx : x ≤ i ⊔ j
⊢ x = x ⊓ i ⊔ x ⊓ j

Tactic:
calc
  x = x ⊓ (i ⊔ j) := left_eq_inf.mpr hx
  _ = x ⊓ i ⊔ x ⊓ j := inf_sup_left _ _ _

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/Kernels.lean
theorem map_lift_kernelComparison [HasKernel f] [HasKernel (G.map f)] {Z : C} {h : Z ⟶ X}
    (w : h ≫ f = 0) :
    G.map (kernel.lift _ h w) ≫ kernelComparison f G =
      kernel.lift _ (G.map h) (by simp only [← G.map_comp, w, Functor.map_zero])

Proof state:
C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : HasZeroMorphisms D
G : C ⥤ D
inst✝² : G.PreservesZeroMorphisms
inst✝¹ : HasKernel f
inst✝ : HasKernel (G.map f)
Z : C
h : Z ⟶ X
w : h ≫ f = 0
⊢ G.map h ≫ G.map f = 0

Tactic:
simp only [← G.map_comp, w, Functor.map_zero]

Result:
no goals

Proof state:
C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : HasZeroMorphisms D
G : C ⥤ D
inst✝² : G.PreservesZeroMorphisms
inst✝¹ : HasKernel f
inst✝ : HasKernel (G.map f)
Z : C
h : Z ⟶ X
w : h ≫ f = 0
⊢ G.map (kernel.lift f h w) ≫ kernelComparison f G = kernel.lift (G.map f) (G.map h) ⋯

Tactic:
ext

Result:
case h
C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : HasZeroMorphisms D
G : C ⥤ D
inst✝² : G.PreservesZeroMorphisms
inst✝¹ : HasKernel f
inst✝ : HasKernel (G.map f)
Z : C
h : Z ⟶ X
w : h ≫ f = 0
⊢ (G.map (kernel.lift f h w) ≫ kernelComparison f G) ≫ equalizer.ι (G.map f) 0 =
    kernel.lift (G.map f) (G.map h) ⋯ ≫ equalizer.ι (G.map f) 0

Proof state:
case h
C : Type u
inst✝⁶ : Category.{v, u} C
inst✝⁵ : HasZeroMorphisms C
X Y : C
f : X ⟶ Y
D : Type u₂
inst✝⁴ : Category.{v₂, u₂} D
inst✝³ : HasZeroMorphisms D
G : C ⥤ D
inst✝² : G.PreservesZeroMorphisms
inst✝¹ : HasKernel f
inst✝ : HasKernel (G.map f)
Z : C
h : Z ⟶ X
w : h ≫ f = 0
⊢ (G.map (kernel.lift f h w) ≫ kernelComparison f G) ≫ equalizer.ι (G.map f) 0 =
    kernel.lift (G.map f) (G.map h) ⋯ ≫ equalizer.ι (G.map f) 0

Tactic:
simp [← G.map_comp]

Result:
no goals
-- Mathlib/Data/Set/Finite/Basic.lean
theorem toFinset_univ [Fintype α] (h : (Set.univ : Set α).Finite) :
    h.toFinset = Finset.univ

Proof state:
α : Type u
inst✝ : Fintype α
h : univ.Finite
⊢ h.toFinset = Finset.univ

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/Calculus/FDeriv/Measurable.lean
theorem isOpen_B {K : Set (E →L[𝕜] F)} {r s ε : ℝ} : IsOpen (B f K r s ε)

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
K : Set (E →L[𝕜] F)
r s ε : ℝ
⊢ IsOpen (B f K r s ε)

Tactic:
simp [B, isOpen_biUnion, IsOpen.inter, isOpen_A]

Result:
no goals
-- Mathlib/RingTheory/MvPolynomial/Symmetric/Defs.lean
theorem esymm_one : esymm σ R 1 = ∑ i, X i

Proof state:
σ : Type u_5
R : Type u_6
inst✝¹ : CommSemiring R
inst✝ : Fintype σ
⊢ esymm σ R 1 = ∑ i : σ, X i

Tactic:
simp [esymm, powersetCard_one]

Result:
no goals
-- Mathlib/Algebra/Order/ToIntervalMod.lean
theorem toIocDiv_zsmul_add (a b : α) (m : ℤ) : toIocDiv hp a (m • p + b) = m + toIocDiv hp a b

Proof state:
α : Type u_1
inst✝ : LinearOrderedAddCommGroup α
hα : Archimedean α
p : α
hp : 0 < p
a b : α
m : ℤ
⊢ toIocDiv hp a (m • p + b) = m + toIocDiv hp a b

Tactic:
rw [add_comm, toIocDiv_add_zsmul, add_comm]

Result:
no goals
-- Mathlib/Analysis/SumIntegralComparisons.lean
theorem AntitoneOn.sum_le_integral_Ico (hab : a ≤ b) (hf : AntitoneOn f (Set.Icc a b)) :
    (∑ i ∈ Finset.Ico a b, f (i + 1 : ℕ)) ≤ ∫ x in a..b, f x

Proof state:
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
⊢ ∑ i ∈ Finset.Ico (0 + a) (b - a + a), f ↑(i + 1) ≤ ∫ (x : ℝ) in ↑a..↑a + ↑(b - a), f x

Tactic:
rw [← Finset.sum_Ico_add, Nat.Ico_zero_eq_range]

Result:
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
⊢ ∑ x ∈ Finset.range (b - a), f ↑(a + x + 1) ≤ ∫ (x : ℝ) in ↑a..↑a + ↑(b - a), f x

Proof state:
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
⊢ ∑ x ∈ Finset.range (b - a), f (↑a + ↑(x + 1)) ≤ ∫ (x : ℝ) in ↑a..↑a + ↑(b - a), f x

Tactic:
apply AntitoneOn.sum_le_integral

Result:
case hf
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
⊢ AntitoneOn f (Icc (↑a) (↑a + ↑(b - a)))

Proof state:
case hf
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
⊢ AntitoneOn f (Icc (↑a) (↑a + ↑(b - a)))

Tactic:
simp only [hf, hab, Nat.cast_sub, add_sub_cancel]

Result:
no goals

Proof state:
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
⊢ ∑ i ∈ Finset.Ico a b, f ↑(i + 1) ≤ ∫ (x : ℝ) in ↑a..↑b, f x

Tactic:
rw [(Nat.sub_add_cancel hab).symm, Nat.cast_add]

Result:
a b : ℕ
f : ℝ → ℝ
hab : a ≤ b
hf : AntitoneOn f (Icc ↑a ↑b)
⊢ ∑ i ∈ Finset.Ico a (b - a + a), f ↑(i + 1) ≤ ∫ (x : ℝ) in ↑a..↑(b - a) + ↑a, f x
-- Mathlib/SetTheory/Game/PGame.lean
theorem moveLeft_neg_symm' {x : PGame} (i) :
    x.moveLeft i = -(-x).moveRight (toRightMovesNeg i)

Proof state:
x : PGame
i : x.LeftMoves
⊢ x.moveLeft i = -(-x).moveRight (toRightMovesNeg i)

Tactic:
simp

Result:
no goals
-- Mathlib/Order/LiminfLimsup.lean
theorem blimsup_true (f : Filter β) (u : β → α) : (blimsup u f fun _ => True) = limsup u f

Proof state:
α : Type u_1
β : Type u_2
inst✝ : ConditionallyCompleteLattice α
f : Filter β
u : β → α
⊢ (blimsup u f fun x => True) = limsup u f

Tactic:
simp [blimsup_eq, limsup_eq]

Result:
no goals
-- Mathlib/Algebra/Group/Indicator.lean
theorem mulIndicator_mul_eq_right {f g : α → M} (h : Disjoint (mulSupport f) (mulSupport g)) :
    (mulSupport g).mulIndicator (f * g) = g

Proof state:
α : Type u_1
M : Type u_3
inst✝ : MulOneClass M
f g : α → M
h : Disjoint (mulSupport f) (mulSupport g)
x : α
hx : x ∈ mulSupport g
this : f x = 1
⊢ (f * g) x = g x

Tactic:
rw [Pi.mul_apply, this, one_mul]

Result:
no goals

Proof state:
α : Type u_1
M : Type u_3
inst✝ : MulOneClass M
f g : α → M
h : Disjoint (mulSupport f) (mulSupport g)
⊢ (mulSupport g).mulIndicator (f * g) = g

Tactic:
refine (mulIndicator_congr fun x hx => ?_).trans mulIndicator_mulSupport

Result:
α : Type u_1
M : Type u_3
inst✝ : MulOneClass M
f g : α → M
h : Disjoint (mulSupport f) (mulSupport g)
x : α
hx : x ∈ mulSupport g
⊢ (f * g) x = g x

Proof state:
α : Type u_1
M : Type u_3
inst✝ : MulOneClass M
f g : α → M
h : Disjoint (mulSupport f) (mulSupport g)
x : α
hx : x ∈ mulSupport g
⊢ (f * g) x = g x

Tactic:
have : f x = 1 := nmem_mulSupport.1 (disjoint_right.1 h hx)

Result:
α : Type u_1
M : Type u_3
inst✝ : MulOneClass M
f g : α → M
h : Disjoint (mulSupport f) (mulSupport g)
x : α
hx : x ∈ mulSupport g
this : f x = 1
⊢ (f * g) x = g x
-- Mathlib/Order/Interval/Set/Basic.lean
theorem Ioc_insert_left (h : a ≤ b) : insert a (Ioc a b) = Icc a b

Proof state:
α : Type u_1
inst✝ : PartialOrder α
a b : α
h : a ≤ b
⊢ insert a (Ioc a b) = Icc a b

Tactic:
rw [insert_eq, union_comm, Ioc_union_left h]

Result:
no goals
-- Mathlib/Algebra/Module/LocalizedModule/Submodule.lean
lemma ker_localizedMap_eq_localized'_ker (g : M →ₗ[R] P) :
    ker (map p f f' g) = ((ker g).localized' S p f).restrictScalars _

Proof state:
case h
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁷ : CommSemiring R
inst✝¹⁶ : CommSemiring S
inst✝¹⁵ : AddCommMonoid M
inst✝¹⁴ : AddCommMonoid N
inst✝¹³ : Module R M
inst✝¹² : Module R N
inst✝¹¹ : Algebra R S
inst✝¹⁰ : Module S N
inst✝⁹ : IsScalarTower R S N
p : Submonoid R
inst✝⁸ : IsLocalization p S
f : M →ₗ[R] N
inst✝⁷ : IsLocalizedModule p f
P : Type u_5
inst✝⁶ : AddCommMonoid P
inst✝⁵ : Module R P
Q : Type u_6
inst✝⁴ : AddCommMonoid Q
inst✝³ : Module R Q
inst✝² : Module S Q
inst✝¹ : IsScalarTower R S Q
f' : P →ₗ[R] Q
inst✝ : IsLocalizedModule p f'
g : M →ₗ[R] P
x✝ : N
⊢ x✝ ∈ ker ((IsLocalizedModule.map p f f') g) ↔ x✝ ∈ Submodule.restrictScalars R (localized' S p f (ker g))

Tactic:
simp [localized'_ker_eq_ker_localizedMap S p f f']

Result:
no goals

Proof state:
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁷ : CommSemiring R
inst✝¹⁶ : CommSemiring S
inst✝¹⁵ : AddCommMonoid M
inst✝¹⁴ : AddCommMonoid N
inst✝¹³ : Module R M
inst✝¹² : Module R N
inst✝¹¹ : Algebra R S
inst✝¹⁰ : Module S N
inst✝⁹ : IsScalarTower R S N
p : Submonoid R
inst✝⁸ : IsLocalization p S
f : M →ₗ[R] N
inst✝⁷ : IsLocalizedModule p f
P : Type u_5
inst✝⁶ : AddCommMonoid P
inst✝⁵ : Module R P
Q : Type u_6
inst✝⁴ : AddCommMonoid Q
inst✝³ : Module R Q
inst✝² : Module S Q
inst✝¹ : IsScalarTower R S Q
f' : P →ₗ[R] Q
inst✝ : IsLocalizedModule p f'
g : M →ₗ[R] P
⊢ ker ((IsLocalizedModule.map p f f') g) = Submodule.restrictScalars R (localized' S p f (ker g))

Tactic:
ext

Result:
case h
R : Type u_1
S : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁷ : CommSemiring R
inst✝¹⁶ : CommSemiring S
inst✝¹⁵ : AddCommMonoid M
inst✝¹⁴ : AddCommMonoid N
inst✝¹³ : Module R M
inst✝¹² : Module R N
inst✝¹¹ : Algebra R S
inst✝¹⁰ : Module S N
inst✝⁹ : IsScalarTower R S N
p : Submonoid R
inst✝⁸ : IsLocalization p S
f : M →ₗ[R] N
inst✝⁷ : IsLocalizedModule p f
P : Type u_5
inst✝⁶ : AddCommMonoid P
inst✝⁵ : Module R P
Q : Type u_6
inst✝⁴ : AddCommMonoid Q
inst✝³ : Module R Q
inst✝² : Module S Q
inst✝¹ : IsScalarTower R S Q
f' : P →ₗ[R] Q
inst✝ : IsLocalizedModule p f'
g : M →ₗ[R] P
x✝ : N
⊢ x✝ ∈ ker ((IsLocalizedModule.map p f f') g) ↔ x✝ ∈ Submodule.restrictScalars R (localized' S p f (ker g))
-- Mathlib/Algebra/AddConstMap/Basic.lean
theorem map_add_zsmul [AddGroup G] [AddGroup H] [AddConstMapClass F G H a b]
    (f : F) (x : G) : ∀ n : ℤ, f (x + n • a) = f x + n • b
  | (n : ℕ) => by simp
  | .negSucc n => by simp [← sub_eq_add_neg]

Proof state:
F : Type u_1
G : Type u_2
H : Type u_3
inst✝³ : FunLike F G H
a : G
b : H
inst✝² : AddGroup G
inst✝¹ : AddGroup H
inst✝ : AddConstMapClass F G H a b
f : F
x : G
n : ℕ
⊢ f (x + ↑n • a) = f x + ↑n • b

Tactic:
simp

Result:
no goals

Proof state:
F : Type u_1
G : Type u_2
H : Type u_3
inst✝³ : FunLike F G H
a : G
b : H
inst✝² : AddGroup G
inst✝¹ : AddGroup H
inst✝ : AddConstMapClass F G H a b
f : F
x : G
n : ℕ
⊢ f (x + Int.negSucc n • a) = f x + Int.negSucc n • b

Tactic:
simp [← sub_eq_add_neg]

Result:
no goals
-- Mathlib/GroupTheory/Perm/Cycle/Factors.lean
theorem cycleFactorsFinset_eq_finset {σ : Perm α} {s : Finset (Perm α)} :
    σ.cycleFactorsFinset = s ↔
      (∀ f : Perm α, f ∈ s → f.IsCycle) ∧
        ∃ h : (s : Set (Perm α)).Pairwise Disjoint,
          s.noncommProd id (h.mono' fun _ _ => Disjoint.commute) = σ

Proof state:
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ : Perm α
s : Finset (Perm α)
⊢ σ.cycleFactorsFinset = s ↔ (∀ f ∈ s, f.IsCycle) ∧ ∃ (h : (↑s).Pairwise Disjoint), s.noncommProd id ⋯ = σ

Tactic:
obtain ⟨l, hl, rfl⟩ := s.exists_list_nodup_eq

Result:
case intro.intro
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ : Perm α
l : List (Perm α)
hl : l.Nodup
⊢ σ.cycleFactorsFinset = l.toFinset ↔
    (∀ f ∈ l.toFinset, f.IsCycle) ∧ ∃ (h : (↑l.toFinset).Pairwise Disjoint), l.toFinset.noncommProd id ⋯ = σ

Proof state:
case intro.intro
α : Type u_2
inst✝¹ : DecidableEq α
inst✝ : Fintype α
σ : Perm α
l : List (Perm α)
hl : l.Nodup
⊢ σ.cycleFactorsFinset = l.toFinset ↔
    (∀ f ∈ l.toFinset, f.IsCycle) ∧ ∃ (h : (↑l.toFinset).Pairwise Disjoint), l.toFinset.noncommProd id ⋯ = σ

Tactic:
simp [cycleFactorsFinset_eq_list_toFinset, hl]

Result:
no goals
-- Mathlib/Probability/Moments/IntegrableExpMul.lean
/-- If 0 belongs to the interior of the interval `integrableExpSet X μ`,
then `|X| ^ n` is integrable for all `n : ℕ`. -/
lemma integrable_pow_abs_of_mem_interior_integrableExpSet
    (h : 0 ∈ interior (integrableExpSet X μ)) (n : ℕ) :
    Integrable (fun ω ↦ |X ω| ^ n) μ

Proof state:
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
h : 0 ∈ interior (integrableExpSet X μ)
n : ℕ
⊢ Integrable (fun ω => |X ω| ^ n) μ

Tactic:
convert integrable_pow_abs_mul_exp_of_mem_interior_integrableExpSet h n

Result:
case h.e'_6.h
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
h : 0 ∈ interior (integrableExpSet X μ)
n : ℕ
x✝ : Ω
⊢ |X x✝| ^ n = |X x✝| ^ n * rexp (0 * X x✝)

Proof state:
case h.e'_6.h
Ω : Type u_1
m : MeasurableSpace Ω
X : Ω → ℝ
μ : Measure Ω
h : 0 ∈ interior (integrableExpSet X μ)
n : ℕ
x✝ : Ω
⊢ |X x✝| ^ n = |X x✝| ^ n * rexp (0 * X x✝)

Tactic:
simp

Result:
no goals
-- Mathlib/Data/Finset/Union.lean
@[simp] lemma disjiUnion_filter_eq (s : Finset α) (t : Finset β) (f : α → β) :
    t.disjiUnion (fun a ↦ s.filter (f · = a)) pairwiseDisjoint_fibers =
      s.filter fun c ↦ f c ∈ t :=
  ext fun b => by simpa using and_comm

Proof state:
α : Type u_1
β : Type u_2
inst✝ : DecidableEq β
s : Finset α
t : Finset β
f : α → β
b : α
⊢ b ∈ t.disjiUnion (fun a => filter (fun x => f x = a) s) ⋯ ↔ b ∈ filter (fun c => f c ∈ t) s

Tactic:
simpa using and_comm

Result:
no goals
-- Mathlib/Data/Set/Prod.lean
theorem empty_prod : (∅ : Set α) ×ˢ t = ∅

Proof state:
α : Type u_1
β : Type u_2
t : Set β
⊢ ∅ ×ˢ t = ∅

Tactic:
ext

Result:
case h
α : Type u_1
β : Type u_2
t : Set β
x✝ : α × β
⊢ x✝ ∈ ∅ ×ˢ t ↔ x✝ ∈ ∅

Proof state:
case h
α : Type u_1
β : Type u_2
t : Set β
x✝ : α × β
⊢ x✝ ∈ ∅ ×ˢ t ↔ x✝ ∈ ∅

Tactic:
exact iff_of_eq (false_and _)

Result:
no goals
-- Mathlib/Data/Set/Pairwise/Basic.lean
theorem pairwise_insert_of_symmetric (hr : Symmetric r) :
    (insert a s).Pairwise r ↔ s.Pairwise r ∧ ∀ b ∈ s, a ≠ b → r a b

Proof state:
α : Type u_1
r : α → α → Prop
s : Set α
a : α
hr : Symmetric r
⊢ (insert a s).Pairwise r ↔ s.Pairwise r ∧ ∀ b ∈ s, a ≠ b → r a b

Tactic:
simp only [pairwise_insert, hr.iff a, and_self_iff]

Result:
no goals
-- Mathlib/RingTheory/LaurentSeries.lean
theorem coe_X : ((X : RatFunc F) : F⸨X⸩) = single 1 1

Proof state:
F : Type u
inst✝ : Field F
⊢ (ofPowerSeries ℤ F) PowerSeries.X = (single 1) 1

Tactic:
simp only [ofPowerSeries_X]

Result:
no goals

Proof state:
F : Type u
inst✝ : Field F
⊢ ↑X = (single 1) 1

Tactic:
rw [coe_num_denom, num_X, denom_X, Polynomial.coe_X, Polynomial.coe_one,
   PowerSeries.coe_one, div_one]

Result:
F : Type u
inst✝ : Field F
⊢ (ofPowerSeries ℤ F) PowerSeries.X = (single 1) 1
-- Mathlib/Analysis/Seminorm.lean
theorem continuous_of_le [TopologicalSpace E] [IsTopologicalAddGroup E]
    {p q : Seminorm 𝕝 E} (hq : Continuous q) (hpq : p ≤ q) : Continuous p

Proof state:
𝕝 : Type u_6
E : Type u_7
inst✝⁴ : SeminormedRing 𝕝
inst✝³ : AddCommGroup E
inst✝² : Module 𝕝 E
inst✝¹ : TopologicalSpace E
inst✝ : IsTopologicalAddGroup E
p q : Seminorm 𝕝 E
hq : Continuous ⇑q
hpq : p ≤ q
⊢ Continuous ⇑p

Tactic:
refine Seminorm.continuous_of_forall (fun r hr ↦ Filter.mem_of_superset
  (IsOpen.mem_nhds ?_ <| q.mem_ball_self hr) (ball_antitone hpq))

Result:
𝕝 : Type u_6
E : Type u_7
inst✝⁴ : SeminormedRing 𝕝
inst✝³ : AddCommGroup E
inst✝² : Module 𝕝 E
inst✝¹ : TopologicalSpace E
inst✝ : IsTopologicalAddGroup E
p q : Seminorm 𝕝 E
hq : Continuous ⇑q
hpq : p ≤ q
r : ℝ
hr : r > 0
⊢ IsOpen (q.ball 0 r)

Proof state:
𝕝 : Type u_6
E : Type u_7
inst✝⁴ : SeminormedRing 𝕝
inst✝³ : AddCommGroup E
inst✝² : Module 𝕝 E
inst✝¹ : TopologicalSpace E
inst✝ : IsTopologicalAddGroup E
p q : Seminorm 𝕝 E
hq : Continuous ⇑q
hpq : p ≤ q
r : ℝ
hr : r > 0
⊢ IsOpen {y | q y < r}

Tactic:
exact isOpen_lt hq continuous_const

Result:
no goals

Proof state:
𝕝 : Type u_6
E : Type u_7
inst✝⁴ : SeminormedRing 𝕝
inst✝³ : AddCommGroup E
inst✝² : Module 𝕝 E
inst✝¹ : TopologicalSpace E
inst✝ : IsTopologicalAddGroup E
p q : Seminorm 𝕝 E
hq : Continuous ⇑q
hpq : p ≤ q
r : ℝ
hr : r > 0
⊢ IsOpen (q.ball 0 r)

Tactic:
rw [ball_zero_eq]

Result:
𝕝 : Type u_6
E : Type u_7
inst✝⁴ : SeminormedRing 𝕝
inst✝³ : AddCommGroup E
inst✝² : Module 𝕝 E
inst✝¹ : TopologicalSpace E
inst✝ : IsTopologicalAddGroup E
p q : Seminorm 𝕝 E
hq : Continuous ⇑q
hpq : p ≤ q
r : ℝ
hr : r > 0
⊢ IsOpen {y | q y < r}