harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/BoxIntegral/Partition/Basic.lean
theorem iUnion_ofWithBot (boxes : Finset (WithBot (Box ι)))
    (le_of_mem : ∀ J ∈ boxes, (J : WithBot (Box ι)) ≤ I)
    (pairwise_disjoint : Set.Pairwise (boxes : Set (WithBot (Box ι))) Disjoint) :
    (ofWithBot boxes le_of_mem pairwise_disjoint).iUnion = ⋃ J ∈ boxes, ↑J

Proof state:
ι : Type u_1
I : Box ι
boxes : Finset (WithBot (Box ι))
le_of_mem : ∀ J ∈ boxes, J ≤ ↑I
pairwise_disjoint : (↑boxes).Pairwise Disjoint
⊢ ⋃ J, ⋃ (_ : ↑J ∈ boxes), ↑J = ⋃ J ∈ boxes, ↑J

Tactic:
simp only [← Box.biUnion_coe_eq_coe, @iUnion_comm _ _ (Box ι), @iUnion_comm _ _ (@Eq _ _ _),
  iUnion_iUnion_eq_right]

Result:
no goals

Proof state:
ι : Type u_1
I : Box ι
boxes : Finset (WithBot (Box ι))
le_of_mem : ∀ J ∈ boxes, J ≤ ↑I
pairwise_disjoint : (↑boxes).Pairwise Disjoint
this : ⋃ J, ⋃ (_ : ↑J ∈ boxes), ↑J = ⋃ J ∈ boxes, ↑J
⊢ (ofWithBot boxes le_of_mem pairwise_disjoint).iUnion = ⋃ J ∈ boxes, ↑J

Tactic:
simpa [ofWithBot, Prepartition.iUnion]

Result:
no goals

Proof state:
ι : Type u_1
I : Box ι
boxes : Finset (WithBot (Box ι))
le_of_mem : ∀ J ∈ boxes, J ≤ ↑I
pairwise_disjoint : (↑boxes).Pairwise Disjoint
⊢ (ofWithBot boxes le_of_mem pairwise_disjoint).iUnion = ⋃ J ∈ boxes, ↑J

Tactic:
suffices ⋃ (J : Box ι) (_ : ↑J ∈ boxes), ↑J = ⋃ J ∈ boxes, (J : Set (ι → ℝ)) by
  simpa [ofWithBot, Prepartition.iUnion]

Result:
ι : Type u_1
I : Box ι
boxes : Finset (WithBot (Box ι))
le_of_mem : ∀ J ∈ boxes, J ≤ ↑I
pairwise_disjoint : (↑boxes).Pairwise Disjoint
⊢ ⋃ J, ⋃ (_ : ↑J ∈ boxes), ↑J = ⋃ J ∈ boxes, ↑J
-- Mathlib/Topology/Constructions.lean
theorem mem_nhds_prod_iff {x : X} {y : Y} {s : Set (X × Y)} :
    s ∈ 𝓝 (x, y) ↔ ∃ u ∈ 𝓝 x, ∃ v ∈ 𝓝 y, u ×ˢ v ⊆ s

Proof state:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x : X
y : Y
s : Set (X × Y)
⊢ s ∈ 𝓝 (x, y) ↔ ∃ u ∈ 𝓝 x, ∃ v ∈ 𝓝 y, u ×ˢ v ⊆ s

Tactic:
rw [nhds_prod_eq, mem_prod_iff]

Result:
no goals
-- Mathlib/Data/ENNReal/Inv.lean
/-- Very general version for distributivity of multiplication over an infimum.

See `ENNReal.iInf_mul_of_ne` for the special case assuming `a ≠ 0` and `a ≠ ∞`, and
`ENNReal.iInf_mul` for the special case assuming `Nonempty ι`. -/
lemma iInf_mul' (hinfty : a = ∞ → ⨅ i, f i = 0 → ∃ i, f i = 0) (h₀ : a = 0 → Nonempty ι) :
    (⨅ i, f i) * a = ⨅ i, f i * a

Proof state:
ι : Sort u_1
f : ι → ℝ≥0∞
a : ℝ≥0∞
hinfty : a = ⊤ → ⨅ i, f i = 0 → ∃ i, f i = 0
h₀ : a = 0 → Nonempty ι
⊢ (⨅ i, f i) * a = ⨅ i, f i * a

Tactic:
simpa only [mul_comm a] using mul_iInf' hinfty h₀

Result:
no goals
-- Mathlib/Algebra/Regular/Basic.lean
theorem isRegular_mul_and_mul_iff :
    IsRegular (a * b) ∧ IsRegular (b * a) ↔ IsRegular a ∧ IsRegular b

Proof state:
case refine_1
R : Type u_1
inst✝ : Semigroup R
a b : R
⊢ IsRegular (a * b) ∧ IsRegular (b * a) → IsRegular a ∧ IsRegular b

Tactic:
rintro ⟨ab, ba⟩

Result:
case refine_1.intro
R : Type u_1
inst✝ : Semigroup R
a b : R
ab : IsRegular (a * b)
ba : IsRegular (b * a)
⊢ IsRegular a ∧ IsRegular b

Proof state:
case refine_2
R : Type u_1
inst✝ : Semigroup R
a b : R
⊢ IsRegular a ∧ IsRegular b → IsRegular (a * b) ∧ IsRegular (b * a)

Tactic:
rintro ⟨ha, hb⟩

Result:
case refine_2.intro
R : Type u_1
inst✝ : Semigroup R
a b : R
ha : IsRegular a
hb : IsRegular b
⊢ IsRegular (a * b) ∧ IsRegular (b * a)

Proof state:
R : Type u_1
inst✝ : Semigroup R
a b : R
⊢ IsRegular (a * b) ∧ IsRegular (b * a) ↔ IsRegular a ∧ IsRegular b

Tactic:
refine ⟨?_, ?_⟩

Result:
case refine_1
R : Type u_1
inst✝ : Semigroup R
a b : R
⊢ IsRegular (a * b) ∧ IsRegular (b * a) → IsRegular a ∧ IsRegular b

case refine_2
R : Type u_1
inst✝ : Semigroup R
a b : R
⊢ IsRegular a ∧ IsRegular b → IsRegular (a * b) ∧ IsRegular (b * a)

Proof state:
case refine_2.intro
R : Type u_1
inst✝ : Semigroup R
a b : R
ha : IsRegular a
hb : IsRegular b
⊢ IsRegular (a * b) ∧ IsRegular (b * a)

Tactic:
exact ⟨ha.mul hb, hb.mul ha⟩

Result:
no goals

Proof state:
case refine_1.intro
R : Type u_1
inst✝ : Semigroup R
a b : R
ab : IsRegular (a * b)
ba : IsRegular (b * a)
⊢ IsRegular a ∧ IsRegular b

Tactic:
exact
  ⟨⟨IsLeftRegular.of_mul ba.left, IsRightRegular.of_mul ab.right⟩,
    ⟨IsLeftRegular.of_mul ab.left, IsRightRegular.of_mul ba.right⟩⟩

Result:
no goals
-- Mathlib/CategoryTheory/Localization/SmallHom.lean
@[simp]
lemma mk_id_comp [HasSmallLocalizedHom.{w} W X Y] [HasSmallLocalizedHom.{w} W X X]
    (α : SmallHom.{w} W X Y) :
    (mk W (𝟙 X)).comp α = α :=
  (equiv W W.Q).injective (by simp [equiv_comp])

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
W : MorphismProperty C
X Y : C
inst✝¹ : HasSmallLocalizedHom W X Y
inst✝ : HasSmallLocalizedHom W X X
α : SmallHom W X Y
⊢ (equiv W W.Q) ((mk W (𝟙 X)).comp α) = (equiv W W.Q) α

Tactic:
simp [equiv_comp]

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Oriented/Basic.lean
theorem two_zsmul_oangle_smul_right_of_ne_zero (x y : V) {r : ℝ} (hr : r ≠ 0) :
    (2 : ℤ) • o.oangle x (r • y) = (2 : ℤ) • o.oangle x y

Proof state:
V : Type u_1
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : Fact (finrank ℝ V = 2)
o : Orientation ℝ V (Fin 2)
x y : V
r : ℝ
hr : r ≠ 0
⊢ 2 • o.oangle x (r • y) = 2 • o.oangle x y

Tactic:
rcases hr.lt_or_lt with (h | h) <;> simp [h]

Result:
no goals
-- Mathlib/SetTheory/ZFC/Basic.lean
theorem mem_funs {x y f : ZFSet.{u}} : f ∈ funs x y ↔ IsFunc x y f

Proof state:
x y f : ZFSet.{u}
⊢ f ∈ x.funs y ↔ x.IsFunc y f

Tactic:
simp [funs, IsFunc]

Result:
no goals
-- Mathlib/Order/Heyting/Basic.lean
theorem disjoint_compl_compl_left_iff : Disjoint aᶜᶜ b ↔ Disjoint a b

Proof state:
α : Type u_2
inst✝ : HeytingAlgebra α
a b : α
⊢ Disjoint aᶜᶜ b ↔ Disjoint a b

Tactic:
simp_rw [← le_compl_iff_disjoint_left, compl_compl_compl]

Result:
no goals
-- Mathlib/Order/Atoms/Finite.lean
theorem exists_covby_infinite_Iic_of_infinite_Iic [IsStronglyCoatomic α]
    (ha : (Set.Iic a).Infinite) (hfin : {x | x ⋖ a}.Finite) :
    ∃ b, b ⋖ a ∧ (Set.Iic b).Infinite

Proof state:
α : Type u_1
inst✝¹ : PartialOrder α
a : α
inst✝ : IsStronglyCoatomic α
ha : (Set.Iic a).Infinite
hfin : {x | x ⋖ a}.Finite
⊢ ∃ b, b ⋖ a ∧ (Set.Iic b).Infinite

Tactic:
simp_rw [← toDual_covBy_toDual_iff (α := α)] at hfin ⊢

Result:
α : Type u_1
inst✝¹ : PartialOrder α
a : α
inst✝ : IsStronglyCoatomic α
ha : (Set.Iic a).Infinite
hfin : {x | OrderDual.toDual a ⋖ OrderDual.toDual x}.Finite
⊢ ∃ b, OrderDual.toDual a ⋖ OrderDual.toDual b ∧ (Set.Iic b).Infinite

Proof state:
α : Type u_1
inst✝¹ : PartialOrder α
a : α
inst✝ : IsStronglyCoatomic α
ha : (Set.Iic a).Infinite
hfin : {x | OrderDual.toDual a ⋖ OrderDual.toDual x}.Finite
⊢ ∃ b, OrderDual.toDual a ⋖ OrderDual.toDual b ∧ (Set.Iic b).Infinite

Tactic:
exact exists_covby_infinite_Ici_of_infinite_Ici (α := αᵒᵈ) ha hfin

Result:
no goals
-- Mathlib/MeasureTheory/Measure/FiniteMeasureProd.lean
/-- The first marginal of a product probability measure is the first probability measure. -/
@[simp] lemma map_fst_prod : (μ.prod ν).map measurable_fst.aemeasurable = μ

Proof state:
case a
α : Type u_1
inst✝¹ : MeasurableSpace α
β : Type u_2
inst✝ : MeasurableSpace β
μ : ProbabilityMeasure α
ν : ProbabilityMeasure β
⊢ ↑((μ.prod ν).map ⋯) = ↑μ

Tactic:
simp only [val_eq_to_measure, toMeasure_map, toMeasure_prod, Measure.map_fst_prod,
           measure_univ, one_smul]

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : MeasurableSpace α
β : Type u_2
inst✝ : MeasurableSpace β
μ : ProbabilityMeasure α
ν : ProbabilityMeasure β
⊢ (μ.prod ν).map ⋯ = μ

Tactic:
apply Subtype.ext

Result:
case a
α : Type u_1
inst✝¹ : MeasurableSpace α
β : Type u_2
inst✝ : MeasurableSpace β
μ : ProbabilityMeasure α
ν : ProbabilityMeasure β
⊢ ↑((μ.prod ν).map ⋯) = ↑μ
-- Mathlib/Logic/Equiv/PartialEquiv.lean
theorem image_source_inter_eq (s : Set α) :
    e '' (e.source ∩ s) = e.target ∩ e.symm ⁻¹' (e.source ∩ s)

Proof state:
α : Type u_1
β : Type u_2
e : PartialEquiv α β
s : Set α
⊢ ↑e '' (e.source ∩ s) = e.target ∩ ↑e.symm ⁻¹' (e.source ∩ s)

Tactic:
rw [inter_comm, e.leftInvOn.image_inter, image_source_eq_target, inter_comm]

Result:
no goals
-- Mathlib/Order/UpperLower/Basic.lean
theorem mem_iInf₂_iff {f : ∀ i, κ i → UpperSet α} : (a ∈ ⨅ (i) (j), f i j) ↔ ∃ i j, a ∈ f i j

Proof state:
α : Type u_1
ι : Sort u_4
κ : ι → Sort u_5
inst✝ : LE α
a : α
f : (i : ι) → κ i → UpperSet α
⊢ a ∈ ⨅ i, ⨅ j, f i j ↔ ∃ i j, a ∈ f i j

Tactic:
simp_rw [mem_iInf_iff]

Result:
no goals
-- Mathlib/Combinatorics/Derangements/Basic.lean
theorem RemoveNone.mem_fiber (a : Option α) (f : Perm α) :
    f ∈ RemoveNone.fiber a ↔
      ∃ F : Perm (Option α), F ∈ derangements (Option α) ∧ F none = a ∧ removeNone F = f

Proof state:
α : Type u_1
inst✝ : DecidableEq α
a : Option α
f : Perm α
⊢ f ∈ fiber a ↔ ∃ F ∈ derangements (Option α), F none = a ∧ removeNone F = f

Tactic:
simp [RemoveNone.fiber, derangements]

Result:
no goals
-- Mathlib/Data/Matroid/Loop.lean
lemma restrict_loops_eq {R : Set α} (hR : R ⊆ M.E) : (M ↾ R).loops = M.loops ∩ R

Proof state:
α : Type u_1
M : Matroid α
R : Set α
hR : R ⊆ M.E
⊢ (M ↾ R).loops = M.loops ∩ R

Tactic:
rw [restrict_loops_eq', diff_eq_empty.2 hR, union_empty]

Result:
no goals
-- Mathlib/GroupTheory/FreeGroup/Basic.lean
theorem Step.length : ∀ {L₁ L₂ : List (α × Bool)}, Step L₁ L₂ → L₂.length + 2 = L₁.length
  | _, _, @Red.Step.not _ L1 L2 x b => by rw [List.length_append, List.length_append]; rfl

Proof state:
α : Type u
L1 L2 : List (α × Bool)
x : α
b : Bool
⊢ (L1 ++ L2).length + 2 = (L1 ++ (x, b) :: (x, !b) :: L2).length

Tactic:
rw [List.length_append, List.length_append]

Result:
α : Type u
L1 L2 : List (α × Bool)
x : α
b : Bool
⊢ L1.length + L2.length + 2 = L1.length + ((x, b) :: (x, !b) :: L2).length

Proof state:
α : Type u
L1 L2 : List (α × Bool)
x : α
b : Bool
⊢ L1.length + L2.length + 2 = L1.length + ((x, b) :: (x, !b) :: L2).length

Tactic:
rfl

Result:
no goals
-- Mathlib/Data/Nat/Totient.lean
theorem totient_prime_pow {p : ℕ} (hp : p.Prime) {n : ℕ} (hn : 0 < n) :
    φ (p ^ n) = p ^ (n - 1) * (p - 1)

Proof state:
p : ℕ
hp : Prime p
n : ℕ
hn : 0 < n
⊢ φ (p ^ n) = p ^ (n - 1) * (p - 1)

Tactic:
rcases exists_eq_succ_of_ne_zero (pos_iff_ne_zero.1 hn) with ⟨m, rfl⟩

Result:
case intro
p : ℕ
hp : Prime p
m : ℕ
hn : 0 < m.succ
⊢ φ (p ^ m.succ) = p ^ (m.succ - 1) * (p - 1)

Proof state:
case intro
p : ℕ
hp : Prime p
m : ℕ
hn : 0 < m.succ
⊢ φ (p ^ m.succ) = p ^ (m.succ - 1) * (p - 1)

Tactic:
exact totient_prime_pow_succ hp _

Result:
no goals
-- Mathlib/Algebra/Order/Field/Basic.lean
theorem sub_self_div_two (a : α) : a - a / 2 = a / 2

Proof state:
α : Type u_2
inst✝ : LinearOrderedField α
a : α
⊢ a - a / 2 = a / 2

Tactic:
suffices a / 2 + a / 2 - a / 2 = a / 2 by rwa [add_halves] at this

Result:
α : Type u_2
inst✝ : LinearOrderedField α
a : α
⊢ a / 2 + a / 2 - a / 2 = a / 2

Proof state:
α : Type u_2
inst✝ : LinearOrderedField α
a : α
this : a / 2 + a / 2 - a / 2 = a / 2
⊢ a - a / 2 = a / 2

Tactic:
rwa [add_halves] at this

Result:
no goals

Proof state:
α : Type u_2
inst✝ : LinearOrderedField α
a : α
⊢ a / 2 + a / 2 - a / 2 = a / 2

Tactic:
rw [add_sub_cancel_right]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Ord.lean
theorem eq_eq_of_isLE_of_isGE {o : Ordering} : o.isLE → o.isGE → o = .eq

Proof state:
o : Ordering
⊢ o.isLE = true → o.isGE = true → o = eq

Tactic:
cases o <;> simp

Result:
no goals
-- Mathlib/Analysis/Normed/Group/Uniform.lean
theorem LipschitzWith.norm_le_mul' {f : E → F} {K : ℝ≥0} (h : LipschitzWith K f) (hf : f 1 = 1)
    (x) : ‖f x‖ ≤ K * ‖x‖

Proof state:
E : Type u_2
F : Type u_3
inst✝¹ : SeminormedGroup E
inst✝ : SeminormedGroup F
f : E → F
K : ℝ≥0
h : LipschitzWith K f
hf : f 1 = 1
x : E
⊢ ‖f x‖ ≤ ↑K * ‖x‖

Tactic:
simpa only [dist_one_right, hf] using h.dist_le_mul x 1

Result:
no goals
-- Mathlib/Topology/Constructions.lean
theorem IsClosed.prod {s₁ : Set X} {s₂ : Set Y} (h₁ : IsClosed s₁) (h₂ : IsClosed s₂) :
    IsClosed (s₁ ×ˢ s₂) :=
  closure_eq_iff_isClosed.mp <| by simp only [h₁.closure_eq, h₂.closure_eq, closure_prod_eq]

Proof state:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s₁ : Set X
s₂ : Set Y
h₁ : IsClosed s₁
h₂ : IsClosed s₂
⊢ closure (s₁ ×ˢ s₂) = s₁ ×ˢ s₂

Tactic:
simp only [h₁.closure_eq, h₂.closure_eq, closure_prod_eq]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem getD_empty {a : α} {fallback : β} {c} :
    getD (empty c : Raw α (fun _ => β)) a fallback = fallback

Proof state:
α : Type u
inst✝¹ : BEq α
inst✝ : Hashable α
β : Type v
a : α
fallback : β
c : Nat
⊢ getD (empty c) a fallback = fallback

Tactic:
simp_to_raw using Raw₀.Const.getD_empty

Result:
no goals
-- Mathlib/Data/List/Sort.lean
theorem sorted_swap_listMap (e : ra ↪r rb) {l : List α} :
    (l.map e).Sorted (Function.swap rb) ↔ l.Sorted (Function.swap ra)

Proof state:
α : Type u_1
β : Type u_2
ra : α → α → Prop
rb : β → β → Prop
e : ra ↪r rb
l : List α
⊢ Sorted (Function.swap rb) (List.map (⇑e) l) ↔ Sorted (Function.swap ra) l

Tactic:
simp [Sorted, pairwise_map, e.map_rel_iff]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/NormalForms.lean
theorem c₄_of_isShortNF : W.c₄ = -48 * W.a₄

Proof state:
R : Type u_1
inst✝¹ : CommRing R
W : WeierstrassCurve R
inst✝ : W.IsShortNF
⊢ W.c₄ = -48 * W.a₄

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Basic.lean
theorem le_of_add_le_add_left {a b c : Nat} (h : a + b ≤ a + c) : b ≤ c

Proof state:
a b c : Nat
h : a + b ≤ a + c
d : Nat
hd : a + (b + d) = a + c
⊢ b + d = c

Tactic:
apply Nat.add_left_cancel hd

Result:
no goals

Proof state:
a b c : Nat
h : a + b ≤ a + c
d : Nat
hd : a + b + d = a + c
⊢ b + d = c

Tactic:
rw [Nat.add_assoc] at hd

Result:
a b c : Nat
h : a + b ≤ a + c
d : Nat
hd : a + (b + d) = a + c
⊢ b + d = c

Proof state:
a b c : Nat
h : a + b ≤ a + c
d : Nat
hd : a + b + d = a + c
⊢ b ≤ c

Tactic:
apply @le.intro _ _ d

Result:
a b c : Nat
h : a + b ≤ a + c
d : Nat
hd : a + b + d = a + c
⊢ b + d = c

Proof state:
a b c : Nat
h : a + b ≤ a + c
⊢ b ≤ c

Tactic:
match le.dest h with
| ⟨d, hd⟩ =>
  apply @le.intro _ _ d
  rw [Nat.add_assoc] at hd
  apply Nat.add_left_cancel hd

Result:
no goals
-- Mathlib/Algebra/Order/Monoid/Unbundled/Pow.lean
theorem min_le_of_mul_le_sq {a b c : M} (h : a * b ≤ c ^ 2) : min a b ≤ c

Proof state:
M : Type u_3
inst✝³ : Monoid M
inst✝² : LinearOrder M
inst✝¹ : MulLeftStrictMono M
inst✝ : MulRightStrictMono M
a b c : M
h : a * b ≤ c ^ 2
⊢ a ⊓ b ≤ c

Tactic:
simpa using min_le_max_of_mul_le_mul (h.trans_eq <| pow_two _)

Result:
no goals
-- Mathlib/RingTheory/MvPolynomial/Symmetric/FundamentalTheorem.lean
lemma esymmAlgHomMonomial_add {t s : Fin n →₀ ℕ} :
    esymmAlgHomMonomial σ (t + s) r = esymmAlgHomMonomial σ t r * esymmAlgHomMonomial σ s 1

Proof state:
σ : Type u_1
R : Type u_3
n : ℕ
inst✝¹ : CommSemiring R
inst✝ : Fintype σ
r : R
t s : Fin n →₀ ℕ
⊢ esymmAlgHomMonomial σ (t + s) r = esymmAlgHomMonomial σ t r * esymmAlgHomMonomial σ s 1

Tactic:
simp_rw [esymmAlgHomMonomial, esymmAlgHom_apply, ← map_mul, monomial_mul, mul_one]

Result:
no goals
-- Mathlib/CategoryTheory/Subobject/Basic.lean
theorem map_id (x : Subobject X) : (map (𝟙 X)).obj x = x

Proof state:
case h
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
f : MonoOver X
⊢ (map (𝟙 X)).obj (Quotient.mk'' f) = Quotient.mk'' f

Tactic:
exact Quotient.sound ⟨(MonoOver.mapId _).app f⟩

Result:
no goals

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
x : Subobject X
⊢ (map (𝟙 X)).obj x = x

Tactic:
induction' x using Quotient.inductionOn' with f

Result:
case h
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X : C
f : MonoOver X
⊢ (map (𝟙 X)).obj (Quotient.mk'' f) = Quotient.mk'' f
-- Mathlib/Topology/PartialHomeomorph.lean
theorem continuous_iff_continuous_comp_left {f : Z → X} (h : f ⁻¹' e.source = univ) :
    Continuous f ↔ Continuous (e ∘ f)

Proof state:
X : Type u_1
Y : Type u_3
Z : Type u_5
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
e : PartialHomeomorph X Y
f : Z → X
h : f ⁻¹' e.source = univ
⊢ ContinuousOn f univ ↔ ContinuousOn (↑e ∘ f) univ

Tactic:
exact e.continuousOn_iff_continuousOn_comp_left (Eq.symm h).subset

Result:
no goals

Proof state:
X : Type u_1
Y : Type u_3
Z : Type u_5
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
e : PartialHomeomorph X Y
f : Z → X
h : f ⁻¹' e.source = univ
⊢ Continuous f ↔ Continuous (↑e ∘ f)

Tactic:
simp only [continuous_iff_continuousOn_univ]

Result:
X : Type u_1
Y : Type u_3
Z : Type u_5
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
e : PartialHomeomorph X Y
f : Z → X
h : f ⁻¹' e.source = univ
⊢ ContinuousOn f univ ↔ ContinuousOn (↑e ∘ f) univ
-- Mathlib/Algebra/Module/Submodule/Bilinear.lean
theorem map₂_eq_span_image2 (f : M →ₗ[R] N →ₗ[R] P) (p : Submodule R M) (q : Submodule R N) :
    map₂ f p q = span R (Set.image2 (fun m n => f m n) (p : Set M) (q : Set N))

Proof state:
R : Type u_1
M : Type u_2
N : Type u_3
P : Type u_4
inst✝⁶ : CommSemiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M →ₗ[R] N →ₗ[R] P
p : Submodule R M
q : Submodule R N
⊢ map₂ f p q = span R (image2 (fun m n => (f m) n) ↑p ↑q)

Tactic:
rw [← map₂_span_span, span_eq, span_eq]

Result:
no goals
-- Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean
lemma zpow_le_one_of_nonpos₀ (ha : 1 ≤ a) (hn : n ≤ 0) : a ^ n ≤ 1

Proof state:
G₀ : Type u_2
inst✝⁴ : GroupWithZero G₀
inst✝³ : PartialOrder G₀
inst✝² : ZeroLEOneClass G₀
inst✝¹ : PosMulReflectLT G₀
a : G₀
inst✝ : PosMulMono G₀
n : ℤ
ha : 1 ≤ a
hn : n ≤ 0
⊢ a ^ n ≤ 1

Tactic:
simpa using zpow_right_mono₀ ha hn

Result:
no goals
-- Mathlib/RingTheory/FractionalIdeal/Operations.lean
theorem spanFinset_ne_zero {ι : Type*} {s : Finset ι} {f : ι → K} :
    spanFinset R₁ s f ≠ 0 ↔ ∃ j ∈ s, f j ≠ 0

Proof state:
R₁ : Type u_3
inst✝³ : CommRing R₁
K : Type u_4
inst✝² : Field K
inst✝¹ : Algebra R₁ K
inst✝ : IsFractionRing R₁ K
ι : Type u_5
s : Finset ι
f : ι → K
⊢ spanFinset R₁ s f ≠ 0 ↔ ∃ j ∈ s, f j ≠ 0

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/Asymptotics/Lemmas.lean
theorem IsLittleO.tendsto_inv_smul_nhds_zero [Module 𝕜 E'] [BoundedSMul 𝕜 E']
    {f : α → E'} {g : α → 𝕜}
    {l : Filter α} (h : f =o[l] g) : Tendsto (fun x => (g x)⁻¹ • f x) l (𝓝 0)

Proof state:
α : Type u_1
E' : Type u_6
𝕜 : Type u_15
inst✝³ : SeminormedAddCommGroup E'
inst✝² : NormedDivisionRing 𝕜
inst✝¹ : Module 𝕜 E'
inst✝ : BoundedSMul 𝕜 E'
f : α → E'
g : α → 𝕜
l : Filter α
h : f =o[l] g
⊢ Tendsto (fun x => (g x)⁻¹ • f x) l (𝓝 0)

Tactic:
simpa only [div_eq_inv_mul, ← norm_inv, ← norm_smul, ← tendsto_zero_iff_norm_tendsto_zero] using
  h.norm_norm.tendsto_div_nhds_zero

Result:
no goals
-- Mathlib/NumberTheory/Zsqrtd/GaussianInt.lean
theorem norm_mod_lt (x : ℤ[i]) {y : ℤ[i]} (hy : y ≠ 0) : (x % y).norm < y.norm :=
  have : (y : ℂ) ≠ 0

Proof state:
x y : ℤ[i]
hy : y ≠ 0
this : toComplex y ≠ 0
⊢ normSq (toComplex y) * 1 = ↑(norm y)

Tactic:
simp

Result:
no goals

Proof state:
x y : ℤ[i]
hy : y ≠ 0
this : toComplex y ≠ 0
⊢ normSq (toComplex x - toComplex y * toComplex (x / y)) =
    normSq (toComplex y) * normSq (toComplex x / toComplex y - toComplex (x / y))

Tactic:
rw [← normSq_mul, mul_sub, mul_div_cancel₀ _ this]

Result:
no goals

Proof state:
x y : ℤ[i]
hy : y ≠ 0
this : toComplex y ≠ 0
⊢ ↑(norm (x % y)) = normSq (toComplex x - toComplex y * toComplex (x / y))

Tactic:
simp [mod_def]

Result:
no goals

Proof state:
x y : ℤ[i]
hy : y ≠ 0
⊢ toComplex y ≠ 0

Tactic:
rwa [Ne, ← toComplex_zero, toComplex_inj]

Result:
no goals
-- Mathlib/RingTheory/UniqueFactorizationDomain/Basic.lean
theorem WfDvdMonoid.iff_wellFounded_associates [CancelCommMonoidWithZero α] :
    WfDvdMonoid α ↔ WellFoundedLT (Associates α) :=
  ⟨by apply WfDvdMonoid.wellFoundedLT_associates, WfDvdMonoid.of_wellFoundedLT_associates⟩

Proof state:
α : Type u_1
inst✝ : CancelCommMonoidWithZero α
⊢ WfDvdMonoid α → WellFoundedLT (Associates α)

Tactic:
apply WfDvdMonoid.wellFoundedLT_associates

Result:
no goals
-- Mathlib/Data/Finset/Basic.lean
theorem sdiff_singleton_eq_self (ha : a ∉ s) : s \ {a} = s

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s : Finset α
a : α
ha : a ∉ s
⊢ s \ {a} = s

Tactic:
rw [← erase_eq, erase_eq_of_not_mem ha]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Range.lean
theorem range'_eq_append_iff : range' s n = xs ++ ys ↔ ∃ k, k ≤ n ∧ xs = range' s k ∧ ys = range' (s + k) (n - k)

Proof state:
s n : Nat
xs ys : Array Nat
⊢ range' s n = xs ++ ys ↔ ∃ k, k ≤ n ∧ xs = range' s k ∧ ys = range' (s + k) (n - k)

Tactic:
simp [← toList_inj, List.range'_eq_append_iff]

Result:
no goals
-- Mathlib/Algebra/Order/Field/Basic.lean
theorem div_two_sub_self (a : α) : a / 2 - a = -(a / 2)

Proof state:
α : Type u_2
inst✝ : LinearOrderedField α
a : α
⊢ a / 2 - a = -(a / 2)

Tactic:
suffices a / 2 - (a / 2 + a / 2) = -(a / 2) by rwa [add_halves] at this

Result:
α : Type u_2
inst✝ : LinearOrderedField α
a : α
⊢ a / 2 - (a / 2 + a / 2) = -(a / 2)

Proof state:
α : Type u_2
inst✝ : LinearOrderedField α
a : α
this : a / 2 - (a / 2 + a / 2) = -(a / 2)
⊢ a / 2 - a = -(a / 2)

Tactic:
rwa [add_halves] at this

Result:
no goals

Proof state:
α : Type u_2
inst✝ : LinearOrderedField α
a : α
⊢ a / 2 - (a / 2 + a / 2) = -(a / 2)

Tactic:
rw [sub_add_eq_sub_sub, sub_self, zero_sub]

Result:
no goals
-- Mathlib/CategoryTheory/Sites/ConcreteSheafification.lean
theorem sheafifyMap_id (P : Cᵒᵖ ⥤ D) : J.sheafifyMap (𝟙 P) = 𝟙 (J.sheafify P)

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 : Cᵒᵖ ⥤ D
⊢ J.sheafifyMap (𝟙 P) = 𝟙 (J.sheafify P)

Tactic:
dsimp [sheafifyMap, sheafify]

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 : Cᵒᵖ ⥤ D
⊢ J.plusMap (J.plusMap (𝟙 P)) = 𝟙 (J.plusObj (J.plusObj P))

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 : Cᵒᵖ ⥤ D
⊢ J.plusMap (J.plusMap (𝟙 P)) = 𝟙 (J.plusObj (J.plusObj P))

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Order/Field/Basic.lean
private lemma exists_mul_right_lt₀ {a b c : α} (hc : a * b < c) : ∃ b' > b, a * b' < c

Proof state:
α : Type u_2
inst✝ : LinearOrderedField α
a b c : α
hc : a * b < c
⊢ ∃ b' > b, a * b' < c

Tactic:
simp_rw [mul_comm a] at hc ⊢

Result:
α : Type u_2
inst✝ : LinearOrderedField α
a b c : α
hc : b * a < c
⊢ ∃ b' > b, b' * a < c

Proof state:
α : Type u_2
inst✝ : LinearOrderedField α
a b c : α
hc : b * a < c
⊢ ∃ b' > b, b' * a < c

Tactic:
exact exists_mul_left_lt₀ hc

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Lemmas.lean
theorem get!_eq_default [EquivBEq α] [LawfulHashable α] [Inhabited β] {a : α} :
    ¬a ∈ m → get! m a = default

Proof state:
α : Type u
x✝¹ : BEq α
x✝ : Hashable α
β : Type v
m : DHashMap α fun x => β
inst✝² : EquivBEq α
inst✝¹ : LawfulHashable α
inst✝ : Inhabited β
a : α
⊢ ¬a ∈ m → get! m a = default

Tactic:
simpa [mem_iff_contains] using get!_eq_default_of_contains_eq_false

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Lebesgue/Basic.lean
theorem measurableSet_graph (hf : Measurable f) :
    MeasurableSet { p : α × ℝ | p.snd = f p.fst }

Proof state:
α : Type u_1
inst✝ : MeasurableSpace α
f : α → ℝ
hf : Measurable f
⊢ MeasurableSet {p | p.2 = f p.1}

Tactic:
simpa using measurableSet_region_between_cc hf hf MeasurableSet.univ

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Option/Attach.lean
theorem attach_eq_none_iff {o : Option α} : o.attach = none ↔ o = none

Proof state:
α : Type u_1
o : Option α
⊢ o.attach = none ↔ o = none

Tactic:
cases o <;> simp

Result:
no goals