harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/MeasureTheory/Function/ConditionalExpectation/AEMeasurable.lean
theorem lpMeasToLpTrimLie_symm_indicator [one_le_p : Fact (1 ≤ p)] [NormedSpace ℝ F] {hm : m ≤ m0}
    {s : Set α} {μ : Measure α} (hs : MeasurableSet[m] s) (hμs : μ.trim hm s ≠ ∞) (c : F) :
    ((lpMeasToLpTrimLie F ℝ p μ hm).symm (indicatorConstLp p hs hμs c) : Lp F p μ) =
      indicatorConstLp p (hm s hs) ((le_trim hm).trans_lt hμs.lt_top).ne c

Proof state:
case h
α : Type u_1
F : Type u_2
p : ℝ≥0∞
inst✝¹ : NormedAddCommGroup F
m m0 : MeasurableSpace α
one_le_p : Fact (1 ≤ p)
inst✝ : NormedSpace ℝ F
hm : m ≤ m0
s : Set α
μ : Measure α
hs : MeasurableSet s
hμs : (μ.trim hm) s ≠ ⊤
c : F
⊢ ↑↑↑(lpTrimToLpMeas F ℝ p μ hm (indicatorConstLp p hs hμs c)) =ᶠ[ae μ] ↑↑(indicatorConstLp p ⋯ ⋯ c)

Tactic:
refine (lpTrimToLpMeas_ae_eq hm _).trans ?_

Result:
case h
α : Type u_1
F : Type u_2
p : ℝ≥0∞
inst✝¹ : NormedAddCommGroup F
m m0 : MeasurableSpace α
one_le_p : Fact (1 ≤ p)
inst✝ : NormedSpace ℝ F
hm : m ≤ m0
s : Set α
μ : Measure α
hs : MeasurableSet s
hμs : (μ.trim hm) s ≠ ⊤
c : F
⊢ ↑↑(indicatorConstLp p hs hμs c) =ᶠ[ae μ] ↑↑(indicatorConstLp p ⋯ ⋯ c)

Proof state:
case h
α : Type u_1
F : Type u_2
p : ℝ≥0∞
inst✝¹ : NormedAddCommGroup F
m m0 : MeasurableSpace α
one_le_p : Fact (1 ≤ p)
inst✝ : NormedSpace ℝ F
hm : m ≤ m0
s : Set α
μ : Measure α
hs : MeasurableSet s
hμs : (μ.trim hm) s ≠ ⊤
c : F
⊢ ↑↑(indicatorConstLp p hs hμs c) =ᶠ[ae μ] ↑↑(indicatorConstLp p ⋯ ⋯ c)

Tactic:
exact (ae_eq_of_ae_eq_trim indicatorConstLp_coeFn).trans indicatorConstLp_coeFn.symm

Result:
no goals

Proof state:
case h
α : Type u_1
F : Type u_2
p : ℝ≥0∞
inst✝¹ : NormedAddCommGroup F
m m0 : MeasurableSpace α
one_le_p : Fact (1 ≤ p)
inst✝ : NormedSpace ℝ F
hm : m ≤ m0
s : Set α
μ : Measure α
hs : MeasurableSet s
hμs : (μ.trim hm) s ≠ ⊤
c : F
⊢ ↑↑↑((lpMeasToLpTrimLie F ℝ p μ hm).symm (indicatorConstLp p hs hμs c)) =ᶠ[ae μ] ↑↑(indicatorConstLp p ⋯ ⋯ c)

Tactic:
change
  lpTrimToLpMeas F ℝ p μ hm (indicatorConstLp p hs hμs c) =ᵐ[μ]
    (indicatorConstLp p _ _ c : α → F)

Result:
case h
α : Type u_1
F : Type u_2
p : ℝ≥0∞
inst✝¹ : NormedAddCommGroup F
m m0 : MeasurableSpace α
one_le_p : Fact (1 ≤ p)
inst✝ : NormedSpace ℝ F
hm : m ≤ m0
s : Set α
μ : Measure α
hs : MeasurableSet s
hμs : (μ.trim hm) s ≠ ⊤
c : F
⊢ ↑↑↑(lpTrimToLpMeas F ℝ p μ hm (indicatorConstLp p hs hμs c)) =ᶠ[ae μ] ↑↑(indicatorConstLp p ⋯ ⋯ c)

Proof state:
α : Type u_1
F : Type u_2
p : ℝ≥0∞
inst✝¹ : NormedAddCommGroup F
m m0 : MeasurableSpace α
one_le_p : Fact (1 ≤ p)
inst✝ : NormedSpace ℝ F
hm : m ≤ m0
s : Set α
μ : Measure α
hs : MeasurableSet s
hμs : (μ.trim hm) s ≠ ⊤
c : F
⊢ ↑((lpMeasToLpTrimLie F ℝ p μ hm).symm (indicatorConstLp p hs hμs c)) = indicatorConstLp p ⋯ ⋯ c

Tactic:
ext1

Result:
case h
α : Type u_1
F : Type u_2
p : ℝ≥0∞
inst✝¹ : NormedAddCommGroup F
m m0 : MeasurableSpace α
one_le_p : Fact (1 ≤ p)
inst✝ : NormedSpace ℝ F
hm : m ≤ m0
s : Set α
μ : Measure α
hs : MeasurableSet s
hμs : (μ.trim hm) s ≠ ⊤
c : F
⊢ ↑↑↑((lpMeasToLpTrimLie F ℝ p μ hm).symm (indicatorConstLp p hs hμs c)) =ᶠ[ae μ] ↑↑(indicatorConstLp p ⋯ ⋯ c)
-- Mathlib/Algebra/Module/Submodule/Range.lean
theorem submoduleImage_apply_of_le {M' : Type*} [AddCommGroup M'] [Module R M']
    {O : Submodule R M} (ϕ : O →ₗ[R] M') (N : Submodule R M) (hNO : N ≤ O) :
    ϕ.submoduleImage N = range (ϕ.comp (Submodule.inclusion hNO))

Proof state:
R : Type u_1
M : Type u_5
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
M' : Type u_10
inst✝¹ : AddCommGroup M'
inst✝ : Module R M'
O : Submodule R M
ϕ : ↥O →ₗ[R] M'
N : Submodule R M
hNO : N ≤ O
⊢ ϕ.submoduleImage N = range (ϕ ∘ₗ Submodule.inclusion hNO)

Tactic:
rw [submoduleImage, range_comp, Submodule.range_inclusion]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem size_ofList_le [EquivBEq α] [LawfulHashable α]
    {l : List (α × β)} :
    (ofList l).size ≤ l.length

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
β : Type v
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
l : List (α × β)
⊢ (ofList l).size ≤ l.length

Tactic:
simp_to_raw using Raw₀.Const.size_insertMany_empty_list_le

Result:
no goals
-- Mathlib/Algebra/BigOperators/Ring/Finset.lean
/-- The product of `f i - g i` over all of `s` is the sum over the powerset of `s` of the product of
`g` over a subset `t` times the product of `f` over the complement of `t` times `(-1) ^ #t`. -/
lemma prod_sub [DecidableEq ι] (f g : ι → α) (s : Finset ι) :
    ∏ i ∈ s, (f i - g i) = ∑ t ∈ s.powerset, (-1) ^ #t * (∏ i ∈ s \ t, f i) * ∏ i ∈ t, g i

Proof state:
ι : Type u_1
α : Type u_3
inst✝¹ : CommRing α
inst✝ : DecidableEq ι
f g : ι → α
s : Finset ι
⊢ ∏ i ∈ s, (f i - g i) = ∑ t ∈ s.powerset, ((-1) ^ #t * ∏ i ∈ s \ t, f i) * ∏ i ∈ t, g i

Tactic:
simp [sub_eq_neg_add, prod_add, ← prod_const, ← prod_mul_distrib, mul_right_comm]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem map_eq_singleton_iff {f : α → β} {l : Vector α 1} {b : β} :
    map f l = #v[b] ↔ ∃ a, l = #v[a] ∧ f a = b

Proof state:
α : Type u_1
β : Type u_2
f : α → β
l : Vector α 1
b : β
⊢ map f l = { toArray := #[b], size_toArray := ⋯ } ↔ ∃ a, l = { toArray := #[a], size_toArray := ⋯ } ∧ f a = b

Tactic:
cases l

Result:
case mk
α : Type u_1
β : Type u_2
f : α → β
b : β
toArray✝ : Array α
size_toArray✝ : toArray✝.size = 1
⊢ map f { toArray := toArray✝, size_toArray := size_toArray✝ } = { toArray := #[b], size_toArray := ⋯ } ↔
    ∃ a, { toArray := toArray✝, size_toArray := size_toArray✝ } = { toArray := #[a], size_toArray := ⋯ } ∧ f a = b

Proof state:
case mk
α : Type u_1
β : Type u_2
f : α → β
b : β
toArray✝ : Array α
size_toArray✝ : toArray✝.size = 1
⊢ map f { toArray := toArray✝, size_toArray := size_toArray✝ } = { toArray := #[b], size_toArray := ⋯ } ↔
    ∃ a, { toArray := toArray✝, size_toArray := size_toArray✝ } = { toArray := #[a], size_toArray := ⋯ } ∧ f a = b

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Homology/ShortComplex/HomologicalComplex.lean
@[reassoc (attr := simp)]
lemma toCycles_cyclesIsoSc'_hom :
    K.toCycles i j ≫ (K.cyclesIsoSc' i j k hi hk).hom = (K.sc' i j k).toCycles

Proof state:
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
inst✝² : HasZeroMorphisms C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex C c
i j k : ι
hi : c.prev j = i
hk : c.next j = k
inst✝¹ : K.HasHomology j
inst✝ : (K.sc' i j k).HasHomology
⊢ K.toCycles i j ≫ (K.cyclesIsoSc' i j k hi hk).hom = (K.sc' i j k).toCycles

Tactic:
simp only [← cancel_mono (K.sc' i j k).iCycles, assoc, cyclesIsoSc'_hom_iCycles,
  toCycles_i, ShortComplex.toCycles_i, shortComplexFunctor'_obj_f]

Result:
no goals
-- Mathlib/Topology/Algebra/Order/Field.lean
theorem tendsto_zpow_atTop_zero {n : ℤ} (hn : n < 0) :
    Tendsto (fun x : 𝕜 => x ^ n) atTop (𝓝 0)

Proof state:
𝕜 : Type u_1
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
n : ℤ
hn : n < 0
⊢ Tendsto (fun x => x ^ n) atTop (𝓝 0)

Tactic:
lift -n to ℕ using le_of_lt (neg_pos.mpr hn) with N h

Result:
case intro
𝕜 : Type u_1
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
n : ℤ
hn : n < 0
N : ℕ
h : ↑N = -n
⊢ Tendsto (fun x => x ^ n) atTop (𝓝 0)

Proof state:
case intro
𝕜 : Type u_1
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
n : ℤ
N : ℕ
hn : 0 < N
h : ↑N = -n
⊢ Tendsto (fun x => x ^ n) atTop (𝓝 0)

Tactic:
simpa only [h, neg_neg] using tendsto_pow_neg_atTop hn.ne'

Result:
no goals

Proof state:
case intro
𝕜 : Type u_1
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
n : ℤ
hn : n < 0
N : ℕ
h : ↑N = -n
⊢ Tendsto (fun x => x ^ n) atTop (𝓝 0)

Tactic:
rw [← neg_pos, ← h, Nat.cast_pos] at hn

Result:
case intro
𝕜 : Type u_1
inst✝² : LinearOrderedField 𝕜
inst✝¹ : TopologicalSpace 𝕜
inst✝ : OrderTopology 𝕜
n : ℤ
N : ℕ
hn : 0 < N
h : ↑N = -n
⊢ Tendsto (fun x => x ^ n) atTop (𝓝 0)
-- Mathlib/CategoryTheory/Limits/Shapes/Pullback/CommSq.lean
lemma of_id_snd : IsPullback f (𝟙 _) (𝟙 _) f := IsPullback.of_vert_isIso ⟨by simp⟩

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Z : C
f : X ⟶ Z
⊢ f ≫ 𝟙 Z = 𝟙 X ≫ f

Tactic:
simp

Result:
no goals
-- Mathlib/LinearAlgebra/AffineSpace/Combination.lean
theorem affineCombinationSingleWeights_apply_self [DecidableEq ι] (i : ι) :
    affineCombinationSingleWeights k i i = 1

Proof state:
k : Type u_1
inst✝¹ : Ring k
ι : Type u_4
inst✝ : DecidableEq ι
i : ι
⊢ affineCombinationSingleWeights k i i = 1

Tactic:
simp [affineCombinationSingleWeights]

Result:
no goals
-- Mathlib/Data/Ordmap/Ordset.lean
theorem all_node3L {P l x m y r} :
    @All α P (node3L l x m y r) ↔ All P l ∧ P x ∧ All P m ∧ P y ∧ All P r

Proof state:
α : Type u_1
P : α → Prop
l : Ordnode α
x : α
m : Ordnode α
y : α
r : Ordnode α
⊢ All P (l.node3L x m y r) ↔ All P l ∧ P x ∧ All P m ∧ P y ∧ All P r

Tactic:
simp [node3L, all_node', and_assoc]

Result:
no goals
-- Mathlib/Order/BooleanAlgebra.lean
theorem Disjoint.sdiff_eq_of_sup_eq (hi : Disjoint x z) (hs : x ⊔ z = y) : y \ x = z :=
  have h : y ⊓ x = x := inf_eq_right.2 <| le_sup_left.trans hs.le
  sdiff_unique (by rw [h, hs]) (by rw [h, hi.eq_bot])

Proof state:
α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
hi : Disjoint x z
hs : x ⊔ z = y
h : y ⊓ x = x
⊢ y ⊓ x ⊔ z = y

Tactic:
rw [h, hs]

Result:
no goals

Proof state:
α : Type u
x y z : α
inst✝ : GeneralizedBooleanAlgebra α
hi : Disjoint x z
hs : x ⊔ z = y
h : y ⊓ x = x
⊢ y ⊓ x ⊓ z = ⊥

Tactic:
rw [h, hi.eq_bot]

Result:
no goals
-- Mathlib/Combinatorics/Colex.lean
theorem geomSum_injective {n : ℕ} (hn : 2 ≤ n) :
    Function.Injective (fun s : Finset ℕ ↦ ∑ i ∈ s, n ^ i)

Proof state:
n : ℕ
hn : 2 ≤ n
⊢ Injective fun s => ∑ i ∈ s, n ^ i

Tactic:
intro _ _ h

Result:
n : ℕ
hn : 2 ≤ n
a₁✝ a₂✝ : Finset ℕ
h : (fun s => ∑ i ∈ s, n ^ i) a₁✝ = (fun s => ∑ i ∈ s, n ^ i) a₂✝
⊢ a₁✝ = a₂✝

Proof state:
n : ℕ
hn : 2 ≤ n
a₁✝ a₂✝ : Finset ℕ
h : (fun s => ∑ i ∈ s, n ^ i) a₁✝ = (fun s => ∑ i ∈ s, n ^ i) a₂✝
⊢ a₁✝ = a₂✝

Tactic:
rwa [le_antisymm_iff, geomSum_le_geomSum_iff_toColex_le_toColex hn,
  geomSum_le_geomSum_iff_toColex_le_toColex hn, ← le_antisymm_iff, Colex.toColex.injEq] at h

Result:
no goals
-- Mathlib/Data/Option/NAry.lean
theorem map₂_swap (f : α → β → γ) (a : Option α) (b : Option β) :
    map₂ f a b = map₂ (fun a b => f b a) b a

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β → γ
a : Option α
b : Option β
⊢ map₂ f a b = map₂ (fun a b => f b a) b a

Tactic:
cases a <;> cases b <;> rfl

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Arctan.lean
theorem arctan_eq_of_tan_eq {x y : ℝ} (h : tan x = y) (hx : x ∈ Ioo (-(π / 2)) (π / 2)) :
    arctan y = x :=
  injOn_tan (arctan_mem_Ioo _) hx (by rw [tan_arctan, h])

Proof state:
x y : ℝ
h : tan x = y
hx : x ∈ Ioo (-(π / 2)) (π / 2)
⊢ tan (arctan y) = tan x

Tactic:
rw [tan_arctan, h]

Result:
no goals
-- Mathlib/CategoryTheory/Sites/ConcreteSheafification.lean
theorem toSheafify_sheafifyLift {P Q : Cᵒᵖ ⥤ D} (η : P ⟶ Q) (hQ : Presheaf.IsSheaf J Q) :
    J.toSheafify P ≫ sheafifyLift J η hQ = η

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{max v u, w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst✝ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
P Q : Cᵒᵖ ⥤ D
η : P ⟶ Q
hQ : Presheaf.IsSheaf J Q
⊢ (J.toPlus P ≫ J.plusMap (J.toPlus P)) ≫ J.plusLift (J.plusLift η hQ) hQ = η

Tactic:
simp

Result:
no goals

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{max v u, w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst✝ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
P Q : Cᵒᵖ ⥤ D
η : P ⟶ Q
hQ : Presheaf.IsSheaf J Q
⊢ J.toSheafify P ≫ J.sheafifyLift η hQ = η

Tactic:
dsimp only [sheafifyLift, toSheafify]

Result:
C : Type u
inst✝³ : Category.{v, u} C
J : GrothendieckTopology C
D : Type w
inst✝² : Category.{max v u, w} D
inst✝¹ : ∀ (P : Cᵒᵖ ⥤ D) (X : C) (S : J.Cover X), HasMultiequalizer (S.index P)
inst✝ : ∀ (X : C), HasColimitsOfShape (J.Cover X)ᵒᵖ D
P Q : Cᵒᵖ ⥤ D
η : P ⟶ Q
hQ : Presheaf.IsSheaf J Q
⊢ (J.toPlus P ≫ J.plusMap (J.toPlus P)) ≫ J.plusLift (J.plusLift η hQ) hQ = η
-- Mathlib/Order/Hom/Basic.lean
theorem OrderIso.complementedLattice [ComplementedLattice α] (f : α ≃o β) : ComplementedLattice β :=
  ⟨fun x => by
    obtain ⟨y, hy⟩ := exists_isCompl (f.symm x)
    rw [← f.symm_apply_apply y] at hy
    exact ⟨f y, f.symm.isCompl_iff.2 hy⟩⟩

Proof state:
α : Type u_2
β : Type u_3
inst✝⁴ : Lattice α
inst✝³ : Lattice β
inst✝² : BoundedOrder α
inst✝¹ : BoundedOrder β
inst✝ : ComplementedLattice α
f : α ≃o β
x : β
⊢ ∃ b, IsCompl x b

Tactic:
obtain ⟨y, hy⟩ := exists_isCompl (f.symm x)

Result:
case intro
α : Type u_2
β : Type u_3
inst✝⁴ : Lattice α
inst✝³ : Lattice β
inst✝² : BoundedOrder α
inst✝¹ : BoundedOrder β
inst✝ : ComplementedLattice α
f : α ≃o β
x : β
y : α
hy : IsCompl (f.symm x) y
⊢ ∃ b, IsCompl x b

Proof state:
case intro
α : Type u_2
β : Type u_3
inst✝⁴ : Lattice α
inst✝³ : Lattice β
inst✝² : BoundedOrder α
inst✝¹ : BoundedOrder β
inst✝ : ComplementedLattice α
f : α ≃o β
x : β
y : α
hy : IsCompl (f.symm x) y
⊢ ∃ b, IsCompl x b

Tactic:
rw [← f.symm_apply_apply y] at hy

Result:
case intro
α : Type u_2
β : Type u_3
inst✝⁴ : Lattice α
inst✝³ : Lattice β
inst✝² : BoundedOrder α
inst✝¹ : BoundedOrder β
inst✝ : ComplementedLattice α
f : α ≃o β
x : β
y : α
hy : IsCompl (f.symm x) (f.symm (f y))
⊢ ∃ b, IsCompl x b

Proof state:
case intro
α : Type u_2
β : Type u_3
inst✝⁴ : Lattice α
inst✝³ : Lattice β
inst✝² : BoundedOrder α
inst✝¹ : BoundedOrder β
inst✝ : ComplementedLattice α
f : α ≃o β
x : β
y : α
hy : IsCompl (f.symm x) (f.symm (f y))
⊢ ∃ b, IsCompl x b

Tactic:
exact ⟨f y, f.symm.isCompl_iff.2 hy⟩

Result:
no goals
-- Mathlib/Topology/Maps/Basic.lean
theorem isOpenMap_iff_interior : IsOpenMap f ↔ ∀ s, f '' interior s ⊆ interior (f '' s) :=
  ⟨IsOpenMap.image_interior_subset, fun hs u hu =>
    subset_interior_iff_isOpen.mp <|
      calc
        f '' u = f '' interior u

Proof state:
X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
hs : ∀ (s : Set X), f '' interior s ⊆ interior (f '' s)
u : Set X
hu : IsOpen u
⊢ f '' u = f '' interior u

Tactic:
rw [hu.interior_eq]

Result:
no goals
-- Mathlib/Data/PNat/Xgcd.lean
theorem reduce_a {u : XgcdType} (h : u.r = 0) : u.reduce = u.finish

Proof state:
u : XgcdType
h : u.r = 0
⊢ u.reduce = u.finish

Tactic:
rw [reduce]

Result:
u : XgcdType
h : u.r = 0
⊢ (if x : u.r = 0 then u.finish else u.step.reduce.flip) = u.finish

Proof state:
u : XgcdType
h : u.r = 0
⊢ (if x : u.r = 0 then u.finish else u.step.reduce.flip) = u.finish

Tactic:
exact if_pos h

Result:
no goals
-- Mathlib/CategoryTheory/Localization/Monoidal.lean
lemma pentagon_aux₃ {X₁ X₂ X₃ Y₃ : LocalizedMonoidal L W ε} (i : X₃ ≅ Y₃) :
    ((X₁ ⊗ X₂) ◁ i.hom) ≫ (α_ X₁ X₂ Y₃).hom ≫ (X₁ ◁ (X₂ ◁ i.inv)) = (α_ X₁ X₂ X₃).hom

Proof state:
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{u_3, u_1} C
inst✝³ : Category.{u_4, u_2} D
L : C ⥤ D
W : MorphismProperty C
inst✝² : MonoidalCategory C
inst✝¹ : W.IsMonoidal
inst✝ : L.IsLocalization W
unit : D
ε : L.obj (𝟙_ C) ≅ unit
X₁ X₂ X₃ Y₃ : LocalizedMonoidal L W ε
i : X₃ ≅ Y₃
⊢ (X₁ ⊗ X₂) ◁ i.hom ≫ (α_ X₁ X₂ Y₃).hom ≫ X₁ ◁ X₂ ◁ i.inv = (α_ X₁ X₂ X₃).hom

Tactic:
simp only [associator_naturality₃_assoc, ← whiskerLeft_comp,
  Iso.hom_inv_id, whiskerLeft_id, comp_id]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Splits.lean
theorem splits_id_iff_splits {f : K[X]} : (f.map i).Splits (RingHom.id L) ↔ f.Splits i

Proof state:
K : Type v
L : Type w
inst✝¹ : CommRing K
inst✝ : Field L
i : K →+* L
f : K[X]
⊢ Splits (RingHom.id L) (map i f) ↔ Splits i f

Tactic:
rw [splits_map_iff, RingHom.id_comp]

Result:
no goals
-- Mathlib/RingTheory/DedekindDomain/Ideal.lean
theorem coe_ideal_span_singleton_div_self {x : R₁} (hx : x ≠ 0) :
    (Ideal.span ({x} : Set R₁) : FractionalIdeal R₁⁰ K) / Ideal.span ({x} : Set R₁) = 1

Proof state:
K : Type u_3
inst✝⁴ : Field K
R₁ : Type u_4
inst✝³ : CommRing R₁
inst✝² : IsDomain R₁
inst✝¹ : Algebra R₁ K
inst✝ : IsFractionRing R₁ K
x : R₁
hx : x ≠ 0
⊢ ↑(Ideal.span {x}) / ↑(Ideal.span {x}) = 1

Tactic:
rw [coeIdeal_span_singleton,
  spanSingleton_div_self K <|
    (map_ne_zero_iff _ <| FaithfulSMul.algebraMap_injective R₁ K).mpr hx]

Result:
no goals
-- Mathlib/NumberTheory/LSeries/Convergence.lean
/-- If `f` is `O(1)`, then the abscissa of absolute convergence of `f` is bounded above by `1`. -/
lemma LSeries.abscissaOfAbsConv_le_one_of_isBigO_one {f : ℕ → ℂ} (h : f =O[atTop] fun _ ↦ (1 : ℝ)) :
    abscissaOfAbsConv f ≤ 1

Proof state:
f : ℕ → ℂ
h : f =O[atTop] fun x => 1
⊢ f =O[atTop] fun n => ↑n ^ 0

Tactic:
simpa using h

Result:
no goals

Proof state:
f : ℕ → ℂ
h : f =O[atTop] fun x => 1
⊢ abscissaOfAbsConv f ≤ 1

Tactic:
simpa using abscissaOfAbsConv_le_of_isBigO_rpow (x := 0) (by simpa using h)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/PropLemmas.lean
theorem and_rotate : a ∧ b ∧ c ↔ b ∧ c ∧ a

Proof state:
a b c : Prop
⊢ a ∧ b ∧ c ↔ b ∧ c ∧ a

Tactic:
rw [and_left_comm, @and_comm a c]

Result:
no goals
-- Mathlib/Data/Set/NAry.lean
theorem image_image2_antidistrib_left {g : γ → δ} {f' : β' → α → δ} {g' : β → β'}
    (h_antidistrib : ∀ a b, g (f a b) = f' (g' b) a) :
    (image2 f s t).image g = image2 f' (t.image g') s :=
  (image_image2_antidistrib h_antidistrib).trans <| by rw [image_id']

Proof state:
α : Type u_1
β : Type u_3
β' : Type u_4
γ : Type u_5
δ : Type u_7
f : α → β → γ
s : Set α
t : Set β
g : γ → δ
f' : β' → α → δ
g' : β → β'
h_antidistrib : ∀ (a : α) (b : β), g (f a b) = f' (g' b) a
⊢ image2 f' (g' '' t) ((fun a => a) '' s) = image2 f' (g' '' t) s

Tactic:
rw [image_id']

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lex/Lemmas.lean
theorem singleton_lex_singleton [BEq α] {lt : α → α → Bool} : #[a].lex #[b] lt = lt a b

Proof state:
α : Type u_1
a b : α
inst✝ : BEq α
lt : α → α → Bool
⊢ (do
        let r ←
          forIn' { start := 0, stop := min #[a].size #[b].size, step := 1, step_pos := Nat.zero_lt_one }
              ⟨none, PUnit.unit⟩ fun i h r =>
              if lt a b = true then pure (ForInStep.done ⟨some true, PUnit.unit⟩)
              else
                if (a != b) = true then pure (ForInStep.done ⟨some false, PUnit.unit⟩)
                else do
                  pure PUnit.unit
                  pure (ForInStep.yield ⟨none, PUnit.unit⟩)
        match r.fst with
          | none => do
            pure PUnit.unit
            pure (decide (#[a].size < #[b].size))
          | some a => pure a).run =
    lt a b

Tactic:
cases lt a b <;> cases a != b <;> simp [Id.run]

Result:
no goals

Proof state:
α : Type u_1
a b : α
inst✝ : BEq α
lt : α → α → Bool
⊢ #[a].lex #[b] lt = lt a b

Tactic:
simp only [lex, List.getElem_toArray, List.getElem_singleton]

Result:
α : Type u_1
a b : α
inst✝ : BEq α
lt : α → α → Bool
⊢ (do
        let r ←
          forIn' { start := 0, stop := min #[a].size #[b].size, step := 1, step_pos := Nat.zero_lt_one }
              ⟨none, PUnit.unit⟩ fun i h r =>
              if lt a b = true then pure (ForInStep.done ⟨some true, PUnit.unit⟩)
              else
                if (a != b) = true then pure (ForInStep.done ⟨some false, PUnit.unit⟩)
                else do
                  pure PUnit.unit
                  pure (ForInStep.yield ⟨none, PUnit.unit⟩)
        match r.fst with
          | none => do
            pure PUnit.unit
            pure (decide (#[a].size < #[b].size))
          | some a => pure a).run =
    lt a b
-- Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean
lemma rpow_add_natCast' {n : ℕ} (h : y + n ≠ 0) (x : ℝ≥0) : x ^ (y + n) = x ^ y * x ^ n

Proof state:
case a
y : ℝ
n : ℕ
h : y + ↑n ≠ 0
x : ℝ≥0
⊢ ↑(x ^ (y + ↑n)) = ↑(x ^ y * x ^ n)

Tactic:
exact Real.rpow_add_natCast' (mod_cast x.2) h

Result:
no goals

Proof state:
y : ℝ
n : ℕ
h : y + ↑n ≠ 0
x : ℝ≥0
⊢ x ^ (y + ↑n) = x ^ y * x ^ n

Tactic:
ext

Result:
case a
y : ℝ
n : ℕ
h : y + ↑n ≠ 0
x : ℝ≥0
⊢ ↑(x ^ (y + ↑n)) = ↑(x ^ y * x ^ n)
-- Mathlib/Geometry/Euclidean/Circumcenter.lean
theorem circumcenter_reindex {m n : ℕ} (s : Simplex ℝ P m) (e : Fin (m + 1) ≃ Fin (n + 1)) :
    (s.reindex e).circumcenter = s.circumcenter

Proof state:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
m n : ℕ
s : Simplex ℝ P m
e : Fin (m + 1) ≃ Fin (n + 1)
⊢ (s.reindex e).circumcenter = s.circumcenter

Tactic:
simp_rw [circumcenter, circumsphere_reindex]

Result:
no goals
-- Mathlib/AlgebraicGeometry/AffineSpace.lean
@[simp]
lemma SpecIso_inv_appTop_coord (R : CommRingCat.{max u v}) (i) :
    (SpecIso n R).inv.appTop (coord _ i) = (Scheme.ΓSpecIso (.of _)).inv (.X i)

Proof state:
n : Type v
R : CommRingCat
i : n
⊢ (ConcreteCategory.hom (Scheme.ΓSpecIso (CommRingCat.mk✝ (MvPolynomial n ↑R))).inv)
      ((ConcreteCategory.hom (mapEquiv n (Scheme.ΓSpecIso R).symm.commRingCatIsoToRingEquiv).toCommRingCatIso.inv)
        (X i)) =
    (ConcreteCategory.hom (Scheme.ΓSpecIso (CommRingCat.of (MvPolynomial n ↑R))).inv) (X i)

Tactic:
congr 1

Result:
case h.e_6.h
n : Type v
R : CommRingCat
i : n
⊢ (ConcreteCategory.hom (mapEquiv n (Scheme.ΓSpecIso R).symm.commRingCatIsoToRingEquiv).toCommRingCatIso.inv) (X i) =
    X i

Proof state:
n : Type v
R : CommRingCat
i : n
⊢ (ConcreteCategory.hom (Scheme.Hom.appTop (SpecIso n R).inv)) (coord (Spec R) i) =
    (ConcreteCategory.hom (Scheme.ΓSpecIso (CommRingCat.of (MvPolynomial n ↑R))).inv) (X i)

Tactic:
simp only [SpecIso, Iso.trans_inv, Functor.mapIso_inv, Iso.op_inv,
  mapEquiv_symm, RingEquiv.toRingHom_eq_coe, Scheme.Spec_map, Quiver.Hom.unop_op,
  Scheme.comp_coeBase, TopologicalSpace.Opens.map_comp_obj, TopologicalSpace.Opens.map_top,
  Scheme.comp_app, CommRingCat.comp_apply]

Result:
n : Type v
R : CommRingCat
i : n
⊢ (ConcreteCategory.hom
        (Scheme.Hom.app (Spec.map (mapEquiv n (Scheme.ΓSpecIso R).symm.commRingCatIsoToRingEquiv).toCommRingCatIso.inv)
          ⊤))
      ((ConcreteCategory.hom (Scheme.Hom.app (isoOfIsAffine n (Spec R)).inv ⊤)) (coord (Spec R) i)) =
    (ConcreteCategory.hom (Scheme.ΓSpecIso (CommRingCat.of (MvPolynomial n ↑R))).inv) (X i)

Proof state:
n : Type v
R : CommRingCat
i : n
⊢ (ConcreteCategory.hom
        (Scheme.Hom.app (Spec.map (mapEquiv n (Scheme.ΓSpecIso R).symm.commRingCatIsoToRingEquiv).toCommRingCatIso.inv)
          ⊤))
      ((ConcreteCategory.hom (Scheme.Hom.app (isoOfIsAffine n (Spec R)).inv ⊤)) (coord (Spec R) i)) =
    (ConcreteCategory.hom (Scheme.ΓSpecIso (CommRingCat.of (MvPolynomial n ↑R))).inv) (X i)

Tactic:
rw [isoOfIsAffine_inv_appTop_coord, ← CommRingCat.comp_apply, ← Scheme.ΓSpecIso_inv_naturality,
    CommRingCat.comp_apply]

Result:
n : Type v
R : CommRingCat
i : n
⊢ (ConcreteCategory.hom (Scheme.ΓSpecIso (CommRingCat.mk✝ (MvPolynomial n ↑R))).inv)
      ((ConcreteCategory.hom (mapEquiv n (Scheme.ΓSpecIso R).symm.commRingCatIsoToRingEquiv).toCommRingCatIso.inv)
        (X i)) =
    (ConcreteCategory.hom (Scheme.ΓSpecIso (CommRingCat.of (MvPolynomial n ↑R))).inv) (X i)

Proof state:
case h.e_6.h
n : Type v
R : CommRingCat
i : n
⊢ (ConcreteCategory.hom (mapEquiv n (Scheme.ΓSpecIso R).symm.commRingCatIsoToRingEquiv).toCommRingCatIso.inv) (X i) =
    X i

Tactic:
exact map_X _ _

Result:
no goals
-- Mathlib/Algebra/Order/Module/Defs.lean
lemma smul_inv_le_iff_of_neg (h : a < 0) : b₁ ≤ a⁻¹ • b₂ ↔ b₂ ≤ a • b₁

Proof state:
α : Type u_1
β : Type u_2
inst✝³ : LinearOrderedField α
inst✝² : OrderedAddCommGroup β
inst✝¹ : Module α β
a : α
b₁ b₂ : β
inst✝ : PosSMulMono α β
h : a < 0
⊢ b₁ ≤ a⁻¹ • b₂ ↔ b₂ ≤ a • b₁

Tactic:
rw [← smul_le_smul_iff_of_neg_left h, smul_inv_smul₀ h.ne]

Result:
no goals
-- Mathlib/Analysis/Complex/UpperHalfPlane/Basic.lean
theorem normSq_pos (z : ℍ) : 0 < Complex.normSq (z : ℂ)

Proof state:
z : ℍ
⊢ ↑z ≠ 0

Tactic:
exact z.ne_zero

Result:
no goals

Proof state:
z : ℍ
⊢ 0 < Complex.normSq ↑z

Tactic:
rw [Complex.normSq_pos]

Result:
z : ℍ
⊢ ↑z ≠ 0