harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/Homology/Opposite.lean
theorem imageToKernel_op {X Y Z : V} (f : X ⟶ Y) (g : Y ⟶ Z) (w : f ≫ g = 0) :
    imageToKernel g.op f.op (by rw [← op_comp, w, op_zero]) =
      (imageSubobjectIso _ ≪≫ (imageOpOp _).symm).hom ≫
        (cokernel.desc f (factorThruImage g)
              (by rw [← cancel_mono (image.ι g), Category.assoc, image.fac, w, zero_comp])).op ≫
          (kernelSubobjectIso _ ≪≫ kernelOpOp _).inv

Proof state:
V : Type u_1
inst✝¹ : Category.{u_2, u_1} V
inst✝ : Abelian V
X Y Z : V
f : X ⟶ Y
g : Y ⟶ Z
w : f ≫ g = 0
⊢ imageToKernel g.op f.op ⋯ =
    (imageSubobjectIso g.op ≪≫ (imageOpOp g).symm).hom ≫
      (cokernel.desc f (factorThruImage g) ⋯).op ≫ (kernelSubobjectIso f.op ≪≫ kernelOpOp f).inv

Tactic:
ext

Result:
case h
V : Type u_1
inst✝¹ : Category.{u_2, u_1} V
inst✝ : Abelian V
X Y Z : V
f : X ⟶ Y
g : Y ⟶ Z
w : f ≫ g = 0
⊢ imageToKernel g.op f.op ⋯ ≫ (kernelSubobject f.op).arrow =
    ((imageSubobjectIso g.op ≪≫ (imageOpOp g).symm).hom ≫
        (cokernel.desc f (factorThruImage g) ⋯).op ≫ (kernelSubobjectIso f.op ≪≫ kernelOpOp f).inv) ≫
      (kernelSubobject f.op).arrow

Proof state:
case h
V : Type u_1
inst✝¹ : Category.{u_2, u_1} V
inst✝ : Abelian V
X Y Z : V
f : X ⟶ Y
g : Y ⟶ Z
w : f ≫ g = 0
⊢ imageToKernel g.op f.op ⋯ ≫ (kernelSubobject f.op).arrow =
    ((imageSubobjectIso g.op ≪≫ (imageOpOp g).symm).hom ≫
        (cokernel.desc f (factorThruImage g) ⋯).op ≫ (kernelSubobjectIso f.op ≪≫ kernelOpOp f).inv) ≫
      (kernelSubobject f.op).arrow

Tactic:
simp only [Iso.trans_hom, Iso.symm_hom, Iso.trans_inv, kernelOpOp_inv, Category.assoc,
  imageToKernel_arrow, kernelSubobject_arrow', kernel.lift_ι, ← op_comp, cokernel.π_desc,
  ← imageSubobject_arrow, ← imageUnopOp_inv_comp_op_factorThruImage g.op]

Result:
case h
V : Type u_1
inst✝¹ : Category.{u_2, u_1} V
inst✝ : Abelian V
X Y Z : V
f : X ⟶ Y
g : Y ⟶ Z
w : f ≫ g = 0
⊢ (imageSubobjectIso g.op).hom ≫ (imageUnopOp g.op).inv ≫ (factorThruImage g.op.unop).op =
    (imageSubobjectIso g.op).hom ≫ (imageOpOp g).inv ≫ (factorThruImage g).op

Proof state:
V : Type u_1
inst✝¹ : Category.{?u.29, u_1} V
inst✝ : Abelian V
X Y Z : V
f : X ⟶ Y
g : Y ⟶ Z
w : f ≫ g = 0
⊢ f ≫ factorThruImage g = 0

Tactic:
rw [← cancel_mono (image.ι g), Category.assoc, image.fac, w, zero_comp]

Result:
no goals

Proof state:
case h
V : Type u_1
inst✝¹ : Category.{u_2, u_1} V
inst✝ : Abelian V
X Y Z : V
f : X ⟶ Y
g : Y ⟶ Z
w : f ≫ g = 0
⊢ (imageSubobjectIso g.op).hom ≫ (imageUnopOp g.op).inv ≫ (factorThruImage g.op.unop).op =
    (imageSubobjectIso g.op).hom ≫ (imageOpOp g).inv ≫ (factorThruImage g).op

Tactic:
rfl

Result:
no goals

Proof state:
V : Type u_1
inst✝¹ : Category.{?u.29, u_1} V
inst✝ : Abelian V
X Y Z : V
f : X ⟶ Y
g : Y ⟶ Z
w : f ≫ g = 0
⊢ g.op ≫ f.op = 0

Tactic:
rw [← op_comp, w, op_zero]

Result:
no goals
-- Mathlib/Order/Filter/Prod.lean
theorem coprod_inf_prod_le (f₁ f₂ : Filter α) (g₁ g₂ : Filter β) :
    f₁.coprod g₁ ⊓ f₂ ×ˢ g₂ ≤ f₁ ×ˢ g₂ ⊔ f₂ ×ˢ g₁ := calc
  f₁.coprod g₁ ⊓ f₂ ×ˢ g₂
  _ = (f₁ ×ˢ ⊤ ⊔ ⊤ ×ˢ g₁) ⊓ f₂ ×ˢ g₂

Proof state:
α : Type u_1
β : Type u_2
f₁ f₂ : Filter α
g₁ g₂ : Filter β
⊢ f₁.coprod g₁ ⊓ f₂ ×ˢ g₂ = (f₁ ×ˢ ⊤ ⊔ ⊤ ×ˢ g₁) ⊓ f₂ ×ˢ g₂

Tactic:
rw [coprod_eq_prod_top_sup_top_prod]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
f₁ f₂ : Filter α
g₁ g₂ : Filter β
⊢ f₁ ×ˢ ⊤ ⊓ f₂ ×ˢ g₂ ⊔ ⊤ ×ˢ g₁ ⊓ f₂ ×ˢ g₂ = (f₁ ⊓ f₂) ×ˢ g₂ ⊔ f₂ ×ˢ (g₁ ⊓ g₂)

Tactic:
simp [prod_inf_prod]

Result:
no goals
-- Mathlib/Algebra/Order/ToIntervalMod.lean
theorem toIocDiv_eq_sub (a b : α) : toIocDiv hp a b = toIocDiv hp 0 (b - a)

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

Tactic:
rw [toIocDiv_sub_eq_toIocDiv_add, zero_add]

Result:
no goals
-- Mathlib/MeasureTheory/Integral/Lebesgue.lean
lemma setLIntegral_eq_of_support_subset {s : Set α} {f : α → ℝ≥0∞} (hsf : f.support ⊆ s) :
    ∫⁻ x in s, f x ∂μ = ∫⁻ x, f x ∂μ

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ≥0∞
hsf : support f ⊆ s
⊢ ∫⁻ (x : α), f x ∂μ = ∫⁻ (a : α), s.indicator f a ∂μ

Tactic:
congr with x

Result:
case e_f.h
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ≥0∞
hsf : support f ⊆ s
x : α
⊢ f x = s.indicator f x

Proof state:
case neg
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ≥0∞
hsf : support f ⊆ s
x : α
h : x ∉ s
⊢ f x = 0

Tactic:
exact Function.support_subset_iff'.1 hsf x h

Result:
no goals

Proof state:
case pos
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ≥0∞
hsf : support f ⊆ s
x : α
h : x ∈ s
⊢ f x = f x

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ≥0∞
hsf : support f ⊆ s
⊢ ∫⁻ (x : α), f x ∂μ ≤ ∫⁻ (x : α) in s, f x ∂μ

Tactic:
apply le_trans (le_of_eq _) (lintegral_indicator_le _ _)

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ≥0∞
hsf : support f ⊆ s
⊢ ∫⁻ (x : α), f x ∂μ = ∫⁻ (a : α), s.indicator f a ∂μ

Proof state:
case e_f.h
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ≥0∞
hsf : support f ⊆ s
x : α
⊢ f x = if x ∈ s then f x else 0

Tactic:
split_ifs with h

Result:
case pos
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ≥0∞
hsf : support f ⊆ s
x : α
h : x ∈ s
⊢ f x = f x

case neg
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ≥0∞
hsf : support f ⊆ s
x : α
h : x ∉ s
⊢ f x = 0

Proof state:
case e_f.h
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ≥0∞
hsf : support f ⊆ s
x : α
⊢ f x = s.indicator f x

Tactic:
simp only [indicator]

Result:
case e_f.h
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ≥0∞
hsf : support f ⊆ s
x : α
⊢ f x = if x ∈ s then f x else 0

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ≥0∞
hsf : support f ⊆ s
⊢ ∫⁻ (x : α) in s, f x ∂μ = ∫⁻ (x : α), f x ∂μ

Tactic:
apply le_antisymm (setLIntegral_le_lintegral s fun x ↦ f x)

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
s : Set α
f : α → ℝ≥0∞
hsf : support f ⊆ s
⊢ ∫⁻ (x : α), f x ∂μ ≤ ∫⁻ (x : α) in s, f x ∂μ
-- Mathlib/Algebra/Homology/HomotopyCategory/HomComplex.lean
@[simp]
lemma cochain_ofHom_homOf_eq_coe (z : Cocycle F G 0) :
    Cochain.ofHom (homOf z) = (z : Cochain F G 0)

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
F G : CochainComplex C ℤ
z : Cocycle F G 0
⊢ Cochain.ofHom z.homOf = ↑z

Tactic:
simpa only [Cocycle.ext_iff] using ofHom_homOf_eq_self z

Result:
no goals
-- Mathlib/Algebra/Group/Units/Basic.lean
theorem eq_divp_iff_mul_eq {x : α} {u : αˣ} {y : α} : x = y /ₚ u ↔ x * u = y

Proof state:
α : Type u
inst✝ : Monoid α
x : α
u : αˣ
y : α
⊢ x = y /ₚ u ↔ x * ↑u = y

Tactic:
rw [eq_comm, divp_eq_iff_mul_eq]

Result:
no goals
-- Mathlib/Topology/MetricSpace/HausdorffDistance.lean
theorem infEdist_lt_iff {r : ℝ≥0∞} : infEdist x s < r ↔ ∃ y ∈ s, edist x y < r

Proof state:
α : Type u
inst✝ : PseudoEMetricSpace α
x : α
s : Set α
r : ℝ≥0∞
⊢ infEdist x s < r ↔ ∃ y ∈ s, edist x y < r

Tactic:
simp_rw [infEdist, iInf_lt_iff, exists_prop]

Result:
no goals
-- Mathlib/AlgebraicTopology/SimplicialSet/Coskeletal.lean
lemma fac_aux₃ {n : ℕ}
    (s : Cone (proj (op ⦋n⦌) (Truncated.inclusion 2).op ⋙ (Truncated.inclusion 2).op ⋙ X))
    (x : s.pt) (φ : ⦋1⦌ ⟶ ⦋n⦌) :
    X.map φ.op (lift s x) = s.π.app (strArrowMk₂ φ) x

Proof state:
X : SSet
inst✝ : X.StrictSegal
n : ℕ
s : Cone (proj (op ⦋n⦌) (Truncated.inclusion 2).op ⋙ (Truncated.inclusion 2).op ⋙ X)
x : s.pt
φ : ⦋1⦌ ⟶ ⦋n⦌
⊢ 0 ≤ 1

Tactic:
decide

Result:
no goals

Proof state:
X : SSet
inst✝ : X.StrictSegal
n : ℕ
s : Cone (proj (op ⦋n⦌) (Truncated.inclusion 2).op ⋙ (Truncated.inclusion 2).op ⋙ X)
x : s.pt
i j : Fin (n + 1)
hij : i ≤ j
⊢ ↑j ≤ n

Tactic:
omega

Result:
no goals

Proof state:
case intro.intro.intro
X : SSet
inst✝ : X.StrictSegal
n : ℕ
s : Cone (proj (op ⦋n⦌) (Truncated.inclusion 2).op ⋙ (Truncated.inclusion 2).op ⋙ X)
x : s.pt
i j : Fin (n + 1)
hij : i ≤ j
⊢ X.map (mkOfLe i j hij).op (lift s x) = s.π.app (strArrowMk₂ (mkOfLe i j hij) ⋯) x

Tactic:
exact fac_aux₂ _ _ _ _ _ _ (by omega)

Result:
no goals

Proof state:
X : SSet
inst✝ : X.StrictSegal
n : ℕ
s : Cone (proj (op ⦋n⦌) (Truncated.inclusion 2).op ⋙ (Truncated.inclusion 2).op ⋙ X)
x : s.pt
φ : ⦋1⦌ ⟶ ⦋n⦌
⊢ X.map φ.op (lift s x) = s.π.app (strArrowMk₂ φ ⋯) x

Tactic:
obtain ⟨i, j, hij, rfl⟩ : ∃ i j hij, φ = mkOfLe i j hij :=
  ⟨φ.toOrderHom 0, φ.toOrderHom 1, φ.toOrderHom.monotone (by decide),
    Hom.ext_one_left _ _ rfl rfl⟩

Result:
case intro.intro.intro
X : SSet
inst✝ : X.StrictSegal
n : ℕ
s : Cone (proj (op ⦋n⦌) (Truncated.inclusion 2).op ⋙ (Truncated.inclusion 2).op ⋙ X)
x : s.pt
i j : Fin (n + 1)
hij : i ≤ j
⊢ X.map (mkOfLe i j hij).op (lift s x) = s.π.app (strArrowMk₂ (mkOfLe i j hij) ⋯) x
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem forall_mem_flatten {p : α → Prop} {L : Vector (Vector α n) m} :
    (∀ (x) (_ : x ∈ flatten L), p x) ↔ ∀ (l) (_ : l ∈ L) (x) (_ : x ∈ l), p x

Proof state:
α : Type u_1
n m : Nat
p : α → Prop
L : Vector (Vector α n) m
⊢ (∀ (x : α), x ∈ L.flatten → p x) ↔ ∀ (l : Vector α n), l ∈ L → ∀ (x : α), x ∈ l → p x

Tactic:
simp only [mem_flatten, forall_exists_index, and_imp]

Result:
α : Type u_1
n m : Nat
p : α → Prop
L : Vector (Vector α n) m
⊢ (∀ (x : α) (x_1 : Vector α n), x_1 ∈ L → x ∈ x_1 → p x) ↔ ∀ (l : Vector α n), l ∈ L → ∀ (x : α), x ∈ l → p x

Proof state:
case mpr
α : Type u_1
n m : Nat
p : α → Prop
L : Vector (Vector α n) m
⊢ (∀ (l : Vector α n), l ∈ L → ∀ (x : α), x ∈ l → p x) → ∀ (x : α) (x_1 : Vector α n), x_1 ∈ L → x ∈ x_1 → p x

Tactic:
intros

Result:
case mpr
α : Type u_1
n m : Nat
p : α → Prop
L : Vector (Vector α n) m
a✝² : ∀ (l : Vector α n), l ∈ L → ∀ (x : α), x ∈ l → p x
x✝¹ : α
x✝ : Vector α n
a✝¹ : x✝ ∈ L
a✝ : x✝¹ ∈ x✝
⊢ p x✝¹

Proof state:
case mpr
α : Type u_1
n m : Nat
p : α → Prop
L : Vector (Vector α n) m
a✝² : ∀ (l : Vector α n), l ∈ L → ∀ (x : α), x ∈ l → p x
x✝¹ : α
x✝ : Vector α n
a✝¹ : x✝ ∈ L
a✝ : x✝¹ ∈ x✝
⊢ p x✝¹

Tactic:
solve_by_elim

Result:
no goals

Proof state:
α : Type u_1
n m : Nat
p : α → Prop
L : Vector (Vector α n) m
⊢ (∀ (x : α) (x_1 : Vector α n), x_1 ∈ L → x ∈ x_1 → p x) ↔ ∀ (l : Vector α n), l ∈ L → ∀ (x : α), x ∈ l → p x

Tactic:
constructor <;> (intros; solve_by_elim)

Result:
no goals
-- Mathlib/RingTheory/LittleWedderburn.lean
theorem Finite.isDomain_to_isField (D : Type*) [Finite D] [Ring D] [IsDomain D] : IsField D

Proof state:
case intro
D : Type u_1
inst✝² : Finite D
inst✝¹ : Ring D
inst✝ : IsDomain D
val✝ : Fintype D
x✝¹ : DivisionRing D := divisionRingOfIsDomain D
x✝ : Field D := littleWedderburn D
⊢ IsField D

Tactic:
exact Field.toIsField D

Result:
no goals

Proof state:
D : Type u_1
inst✝² : Finite D
inst✝¹ : Ring D
inst✝ : IsDomain D
⊢ IsField D

Tactic:
cases nonempty_fintype D

Result:
case intro
D : Type u_1
inst✝² : Finite D
inst✝¹ : Ring D
inst✝ : IsDomain D
val✝ : Fintype D
⊢ IsField D

Proof state:
case intro
D : Type u_1
inst✝² : Finite D
inst✝¹ : Ring D
inst✝ : IsDomain D
val✝ : Fintype D
x✝ : DivisionRing D := divisionRingOfIsDomain D
⊢ IsField D

Tactic:
let _ := littleWedderburn D

Result:
case intro
D : Type u_1
inst✝² : Finite D
inst✝¹ : Ring D
inst✝ : IsDomain D
val✝ : Fintype D
x✝¹ : DivisionRing D := divisionRingOfIsDomain D
x✝ : Field D := littleWedderburn D
⊢ IsField D

Proof state:
case intro
D : Type u_1
inst✝² : Finite D
inst✝¹ : Ring D
inst✝ : IsDomain D
val✝ : Fintype D
⊢ IsField D

Tactic:
let _ := Fintype.divisionRingOfIsDomain D

Result:
case intro
D : Type u_1
inst✝² : Finite D
inst✝¹ : Ring D
inst✝ : IsDomain D
val✝ : Fintype D
x✝ : DivisionRing D := divisionRingOfIsDomain D
⊢ IsField D

Proof state:
D : Type u_1
inst✝² : Finite D
inst✝¹ : Ring D
inst✝ : IsDomain D
⊢ IsField D

Tactic:
classical
cases nonempty_fintype D
let _ := Fintype.divisionRingOfIsDomain D
let _ := littleWedderburn D
exact Field.toIsField D

Result:
no goals
-- Mathlib/Topology/Partial.lean
theorem pcontinuous_iff' {f : X →. Y} :
    PContinuous f ↔ ∀ {x y} (_ : y ∈ f x), PTendsto' f (𝓝 x) (𝓝 y)

Proof state:
case mp
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X →. Y
⊢ PContinuous f → ∀ {x : X} {y : Y}, y ∈ f x → PTendsto' f (𝓝 x) (𝓝 y)

Tactic:
intro h x y h'

Result:
case mp
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X →. Y
h : PContinuous f
x : X
y : Y
h' : y ∈ f x
⊢ PTendsto' f (𝓝 x) (𝓝 y)

Proof state:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X →. Y
⊢ PContinuous f ↔ ∀ {x : X} {y : Y}, y ∈ f x → PTendsto' f (𝓝 x) (𝓝 y)

Tactic:
constructor

Result:
case mp
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X →. Y
⊢ PContinuous f → ∀ {x : X} {y : Y}, y ∈ f x → PTendsto' f (𝓝 x) (𝓝 y)

case mpr
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X →. Y
⊢ (∀ {x : X} {y : Y}, y ∈ f x → PTendsto' f (𝓝 x) (𝓝 y)) → PContinuous f

Proof state:
case a
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X →. Y
hf : ∀ {x : X} {y : Y}, y ∈ f x → PTendsto' f (𝓝 x) (𝓝 y)
s : Set Y
os : IsOpen s
x : X
y : Y
ys : y ∈ s
fxy : y ∈ f x
t : Set X
h : f.preimage s ⊆ t
h' : ∀ s ∈ 𝓝 y, f.preimage s ∈ 𝓝 x
⊢ ∃ t ⊆ s, IsOpen t ∧ y ∈ t

Tactic:
exact ⟨s, Set.Subset.refl _, os, ys⟩

Result:
no goals

Proof state:
case mp
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X →. Y
h : PContinuous f
x : X
y : Y
h' : y ∈ f x
⊢ ∀ (s : Set Y), (∃ t ⊆ s, IsOpen t ∧ y ∈ t) → ∃ t ⊆ f.preimage s, IsOpen t ∧ x ∈ t

Tactic:
rintro s ⟨t, tsubs, opent, yt⟩

Result:
case mp.intro.intro.intro
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X →. Y
h : PContinuous f
x : X
y : Y
h' : y ∈ f x
s t : Set Y
tsubs : t ⊆ s
opent : IsOpen t
yt : y ∈ t
⊢ ∃ t ⊆ f.preimage s, IsOpen t ∧ x ∈ t

Proof state:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X →. Y
hf : ∀ {x : X} {y : Y}, y ∈ f x → PTendsto' f (𝓝 x) (𝓝 y)
s✝ : Set Y
os : IsOpen s✝
x : X
y : Y
ys : y ∈ s✝
fxy : y ∈ f x
t : Set X
h : f.preimage s✝ ⊆ t
s : Set Y
hs : s ∈ 𝓝 y
this : PTendsto' f (𝓝 x) (𝓝 y)
⊢ f.preimage s ∈ 𝓝 x

Tactic:
rw [ptendsto'_def] at this

Result:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X →. Y
hf : ∀ {x : X} {y : Y}, y ∈ f x → PTendsto' f (𝓝 x) (𝓝 y)
s✝ : Set Y
os : IsOpen s✝
x : X
y : Y
ys : y ∈ s✝
fxy : y ∈ f x
t : Set X
h : f.preimage s✝ ⊆ t
s : Set Y
hs : s ∈ 𝓝 y
this : ∀ s ∈ 𝓝 y, f.preimage s ∈ 𝓝 x
⊢ f.preimage s ∈ 𝓝 x
-- Mathlib/Data/NNRat/Defs.lean
lemma divNat_mul_right {a : ℕ} (ha : a ≠ 0) (n d : ℕ) : divNat (n * a) (d * a) = divNat n d

Proof state:
case a
a : ℕ
ha : a ≠ 0
n d : ℕ
⊢ ↑(divNat (n * a) (d * a)) = ↑(divNat n d)

Tactic:
push_cast

Result:
case a
a : ℕ
ha : a ≠ 0
n d : ℕ
⊢ Rat.divInt (↑n * ↑a) (↑d * ↑a) = Rat.divInt ↑n ↑d

Proof state:
case a
a : ℕ
ha : a ≠ 0
n d : ℕ
⊢ Rat.divInt (↑n * ↑a) (↑d * ↑a) = Rat.divInt ↑n ↑d

Tactic:
exact Rat.divInt_mul_right (mod_cast ha)

Result:
no goals

Proof state:
a : ℕ
ha : a ≠ 0
n d : ℕ
⊢ divNat (n * a) (d * a) = divNat n d

Tactic:
ext

Result:
case a
a : ℕ
ha : a ≠ 0
n d : ℕ
⊢ ↑(divNat (n * a) (d * a)) = ↑(divNat n d)
-- Mathlib/LinearAlgebra/Matrix/Determinant/Basic.lean
theorem det_updateRow_eq_zero (h : i ≠ j) :
    (M.updateRow j (M i)).det = 0 := det_zero_of_row_eq h (by simp [h])

Proof state:
n : Type u_2
inst✝² : DecidableEq n
inst✝¹ : Fintype n
R : Type v
inst✝ : CommRing R
M : Matrix n n R
i j : n
h : i ≠ j
⊢ M.updateRow j (M i) i = M.updateRow j (M i) j

Tactic:
simp [h]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Affine.lean
lemma baseChange_nonsingular (hf : Function.Injective f) :
    (W'.baseChange B).toAffine.Nonsingular (f x) (f y) ↔
      (W'.baseChange A).toAffine.Nonsingular x y

Proof state:
R : Type r
S : Type s
A : Type u
B : Type v
inst✝¹⁰ : CommRing R
inst✝⁹ : CommRing S
inst✝⁸ : CommRing A
inst✝⁷ : CommRing B
W' : Affine R
inst✝⁶ : Algebra R S
inst✝⁵ : Algebra R A
inst✝⁴ : Algebra S A
inst✝³ : IsScalarTower R S A
inst✝² : Algebra R B
inst✝¹ : Algebra S B
inst✝ : IsScalarTower R S B
f : A →ₐ[S] B
x y : A
hf : Function.Injective ⇑f
⊢ (baseChange W' B).toAffine.Nonsingular (f x) (f y) ↔ (baseChange W' A).toAffine.Nonsingular x y

Tactic:
rw [← map_nonsingular _ _ hf, AlgHom.toRingHom_eq_coe, map_baseChange, RingHom.coe_coe]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem ext_getElem? {l₁ l₂ : Array α} (h : ∀ i : Nat, l₁[i]? = l₂[i]?) : l₁ = l₂

Proof state:
case mk.mk
α : Type u_1
l₁ l₂ : List α
h : ∀ (i : Nat), { toList := l₁ }[i]? = { toList := l₂ }[i]?
⊢ { toList := l₁ } = { toList := l₂ }

Tactic:
simpa using List.ext_getElem? (by simpa using h)

Result:
no goals

Proof state:
α : Type u_1
l₁ l₂ : Array α
h : ∀ (i : Nat), l₁[i]? = l₂[i]?
⊢ l₁ = l₂

Tactic:
rcases l₁ with ⟨l₁⟩

Result:
case mk
α : Type u_1
l₂ : Array α
l₁ : List α
h : ∀ (i : Nat), { toList := l₁ }[i]? = l₂[i]?
⊢ { toList := l₁ } = l₂

Proof state:
case mk
α : Type u_1
l₂ : Array α
l₁ : List α
h : ∀ (i : Nat), { toList := l₁ }[i]? = l₂[i]?
⊢ { toList := l₁ } = l₂

Tactic:
rcases l₂ with ⟨l₂⟩

Result:
case mk.mk
α : Type u_1
l₁ l₂ : List α
h : ∀ (i : Nat), { toList := l₁ }[i]? = { toList := l₂ }[i]?
⊢ { toList := l₁ } = { toList := l₂ }

Proof state:
α : Type u_1
l₁ l₂ : List α
h : ∀ (i : Nat), { toList := l₁ }[i]? = { toList := l₂ }[i]?
⊢ ∀ (i : Nat), l₁[i]? = l₂[i]?

Tactic:
simpa using h

Result:
no goals
-- Mathlib/Analysis/Calculus/ContDiff/Basic.lean
theorem contDiffOn_succ_iff_derivWithin (hs : UniqueDiffOn 𝕜 s₂) :
    ContDiffOn 𝕜 (n + 1) f₂ s₂ ↔
      DifferentiableOn 𝕜 f₂ s₂ ∧ (n = ω → AnalyticOn 𝕜 f₂ s₂) ∧
        ContDiffOn 𝕜 n (derivWithin f₂ s₂) s₂

Proof state:
case mp.intro
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n : WithTop ℕ∞
f₂ : 𝕜 → F
s₂ : Set 𝕜
hs : UniqueDiffOn 𝕜 s₂
a✝ : DifferentiableOn 𝕜 f₂ s₂
h' : n = ω → AnalyticOn 𝕜 f₂ s₂
h : ContDiffOn 𝕜 n (fderivWithin 𝕜 f₂ s₂) s₂
⊢ ContDiffOn 𝕜 n (derivWithin f₂ s₂) s₂

Tactic:
have : derivWithin f₂ s₂ = (fun u : 𝕜 →L[𝕜] F => u 1) ∘ fderivWithin 𝕜 f₂ s₂ := by
  ext x; rfl

Result:
case mp.intro
𝕜 : Type u_1
inst✝² : NontriviallyNormedField 𝕜
F : Type uF
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
n : WithTop ℕ∞
f₂ : 𝕜 → F
s₂ : Set 𝕜
hs : UniqueDiffOn 𝕜 s₂
a✝ : DifferentiableOn 𝕜 f₂ s₂
h' : n = ω → AnalyticOn 𝕜 f₂ s₂
h : ContDiffOn 𝕜 n (fderivWithin 𝕜 f₂ s₂) s₂
this : derivWithin f₂ s₂ = (fun u => u 1) ∘ fderivWithin 𝕜 f₂ s₂
⊢ ContDiffOn 𝕜 n (derivWithin f₂ s₂) s₂
-- Mathlib/Tactic/NormNum/BigOperators.lean
lemma Multiset.range_succ' {n nn n' : ℕ} (pn : NormNum.IsNat n nn) (pn' : nn = Nat.succ n') :
    Multiset.range n = n' ::ₘ Multiset.range n'

Proof state:
n nn n' : ℕ
pn : NormNum.IsNat n nn
pn' : nn = n'.succ
⊢ Multiset.range n = n' ::ₘ Multiset.range n'

Tactic:
rw [pn.out, Nat.cast_id, pn', Multiset.range_succ]

Result:
no goals
-- Mathlib/Data/Real/EReal.lean
lemma mul_nonneg_iff {a b : EReal} : 0 ≤ a * b ↔ 0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0

Proof state:
a b : EReal
⊢ 0 ≤ a * b ↔ 0 ≤ a ∧ 0 ≤ b ∨ a ≤ 0 ∧ b ≤ 0

Tactic:
simp_rw [le_iff_lt_or_eq, mul_pos_iff, zero_eq_mul (a := a)]

Result:
a b : EReal
⊢ (0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0) ∨ a = 0 ∨ b = 0 ↔
    (0 < a ∨ 0 = a) ∧ (0 < b ∨ 0 = b) ∨ (a < 0 ∨ a = 0) ∧ (b < 0 ∨ b = 0)

Proof state:
a b : EReal
⊢ (0 < a ∧ 0 < b ∨ a < 0 ∧ b < 0) ∨ a = 0 ∨ b = 0 ↔
    (0 < a ∨ 0 = a) ∧ (0 < b ∨ 0 = b) ∨ (a < 0 ∨ a = 0) ∧ (b < 0 ∨ b = 0)

Tactic:
rcases lt_trichotomy a 0 with (h | h | h) <;> rcases lt_trichotomy b 0 with (h' | h' | h')
  <;> simp only [h, h', true_or, true_and, or_true, and_true] <;> tauto

Result:
no goals
-- Mathlib/Analysis/Complex/UpperHalfPlane/Metric.lean
theorem image_coe_sphere (z : ℍ) (r : ℝ) :
    ((↑) : ℍ → ℂ) '' sphere (α := ℍ) z r = sphere ↑(z.center r) (z.im * Real.sinh r)

Proof state:
case h
z : ℍ
r : ℝ
w : ℂ
⊢ w ∈ UpperHalfPlane.coe '' sphere z r ↔ w ∈ sphere (↑(z.center r)) (z.im * Real.sinh r)

Tactic:
constructor

Result:
case h.mp
z : ℍ
r : ℝ
w : ℂ
⊢ w ∈ UpperHalfPlane.coe '' sphere z r → w ∈ sphere (↑(z.center r)) (z.im * Real.sinh r)

case h.mpr
z : ℍ
r : ℝ
w : ℂ
⊢ w ∈ sphere (↑(z.center r)) (z.im * Real.sinh r) → w ∈ UpperHalfPlane.coe '' sphere z r

Proof state:
case h.mpr.intro
z : ℍ
r : ℝ
w : ℍ
hw : ↑w ∈ sphere (↑(z.center r)) (z.im * Real.sinh r)
⊢ ↑w ∈ UpperHalfPlane.coe '' sphere z r

Tactic:
exact mem_image_of_mem _ (dist_eq_iff_dist_coe_center_eq.2 hw)

Result:
no goals

Proof state:
case h.mp.intro.intro
z : ℍ
r : ℝ
w : ℍ
hw : w ∈ sphere z r
⊢ ↑w ∈ sphere (↑(z.center r)) (z.im * Real.sinh r)

Tactic:
exact dist_eq_iff_dist_coe_center_eq.1 hw

Result:
no goals

Proof state:
case h.mp
z : ℍ
r : ℝ
w : ℂ
⊢ w ∈ UpperHalfPlane.coe '' sphere z r → w ∈ sphere (↑(z.center r)) (z.im * Real.sinh r)

Tactic:
rintro ⟨w, hw, rfl⟩

Result:
case h.mp.intro.intro
z : ℍ
r : ℝ
w : ℍ
hw : w ∈ sphere z r
⊢ ↑w ∈ sphere (↑(z.center r)) (z.im * Real.sinh r)

Proof state:
z : ℍ
r : ℝ
⊢ UpperHalfPlane.coe '' sphere z r = sphere (↑(z.center r)) (z.im * Real.sinh r)

Tactic:
ext w

Result:
case h
z : ℍ
r : ℝ
w : ℂ
⊢ w ∈ UpperHalfPlane.coe '' sphere z r ↔ w ∈ sphere (↑(z.center r)) (z.im * Real.sinh r)

Proof state:
case h.mpr
z : ℍ
r : ℝ
w : ℂ
hw : w ∈ sphere (↑(z.center r)) (z.im * Real.sinh r)
⊢ w ∈ UpperHalfPlane.coe '' sphere z r

Tactic:
lift w to ℍ using im_pos_of_dist_center_le (sphere_subset_closedBall hw)

Result:
case h.mpr.intro
z : ℍ
r : ℝ
w : ℍ
hw : ↑w ∈ sphere (↑(z.center r)) (z.im * Real.sinh r)
⊢ ↑w ∈ UpperHalfPlane.coe '' sphere z r

Proof state:
case h.mpr
z : ℍ
r : ℝ
w : ℂ
⊢ w ∈ sphere (↑(z.center r)) (z.im * Real.sinh r) → w ∈ UpperHalfPlane.coe '' sphere z r

Tactic:
intro hw

Result:
case h.mpr
z : ℍ
r : ℝ
w : ℂ
hw : w ∈ sphere (↑(z.center r)) (z.im * Real.sinh r)
⊢ w ∈ UpperHalfPlane.coe '' sphere z r
-- Mathlib/CategoryTheory/Monoidal/Bimod.lean
theorem one_act_left' : (R.one ▷ _) ≫ actLeft P Q = (λ_ _).hom

Proof state:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : HasCoequalizers C
R S T : Mon_ C
P : Bimod R S
Q : Bimod S T
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
⊢ 𝟙_ C ◁ coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft) ≫
      R.one ▷ coequalizer (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft) ≫ actLeft P Q =
    𝟙_ C ◁ coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft) ≫
      (λ_ (coequalizer (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft))).hom

Tactic:
slice_lhs 1 2 => erw [whisker_exchange]

Result:
C : Type u₁
inst✝³ : Category.{v₁, u₁} C
inst✝² : MonoidalCategory C
inst✝¹ : HasCoequalizers C
R S T : Mon_ C
P : Bimod R S
Q : Bimod S T
inst✝ : ∀ (X : C), PreservesColimitsOfSize.{0, 0, v₁, v₁, u₁, u₁} (tensorLeft X)
⊢ (R.one ▷ (P.X ⊗ Q.X) ≫ R.X ◁ coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft)) ≫
      actLeft P Q =
    𝟙_ C ◁ coequalizer.π (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft) ≫
      (λ_ (coequalizer (P.actRight ▷ Q.X) ((α_ P.X S.X Q.X).hom ≫ P.X ◁ Q.actLeft))).hom
-- Mathlib/CategoryTheory/Localization/HomEquiv.lean
lemma homEquiv_isoOfHom_inv (f : Y ⟶ X) (hf : W f) :
    homEquiv W L₁ L₂ (isoOfHom L₁ W f hf).inv = (isoOfHom L₂ W f hf).inv

Proof state:
C : Type u_1
D₁ : Type u_5
D₂ : Type u_6
inst✝⁴ : Category.{u_8, u_1} C
inst✝³ : Category.{u_10, u_5} D₁
inst✝² : Category.{u_9, u_6} D₂
W : MorphismProperty C
L₁ : C ⥤ D₁
inst✝¹ : L₁.IsLocalization W
L₂ : C ⥤ D₂
inst✝ : L₂.IsLocalization W
X Y : C
f : Y ⟶ X
hf : W f
⊢ (homEquiv W L₁ L₂) (isoOfHom L₁ W f hf).inv = (isoOfHom L₂ W f hf).inv

Tactic:
rw [← cancel_mono (isoOfHom L₂ W f hf).hom, Iso.inv_hom_id, isoOfHom_hom,
  ← homEquiv_map W L₁ L₂ f, ← homEquiv_comp, isoOfHom_inv_hom_id, homEquiv_id]

Result:
no goals