harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/SpecificLimits/Basic.lean
lemma ENNReal.eq_zero_of_le_mul_pow {x r : ℝ≥0∞} {ε : ℝ≥0} (hr : r < 1)
    (h : ∀ n : ℕ, x ≤ ε * r ^ n) : x = 0

Proof state:
x r : ℝ≥0∞
ε : ℝ≥0
hr : r < 1
h : ∀ (n : ℕ), x ≤ ↑ε * r ^ n
⊢ x = 0

Tactic:
rw [← nonpos_iff_eq_zero]

Result:
x r : ℝ≥0∞
ε : ℝ≥0
hr : r < 1
h : ∀ (n : ℕ), x ≤ ↑ε * r ^ n
⊢ x ≤ 0

Proof state:
x r : ℝ≥0∞
ε : ℝ≥0
hr : r < 1
h : ∀ (n : ℕ), x ≤ ↑ε * r ^ n
⊢ x ≤ 0

Tactic:
refine ge_of_tendsto' (f := fun (n : ℕ) ↦ ε * r ^ n) (x := atTop) ?_ h

Result:
x r : ℝ≥0∞
ε : ℝ≥0
hr : r < 1
h : ∀ (n : ℕ), x ≤ ↑ε * r ^ n
⊢ Tendsto (fun n => ↑ε * r ^ n) atTop (𝓝 0)

Proof state:
x r : ℝ≥0∞
ε : ℝ≥0
hr : r < 1
h : ∀ (n : ℕ), x ≤ ↑ε * r ^ n
⊢ Tendsto (fun n => ↑ε * r ^ n) atTop (𝓝 0)

Tactic:
rw [← mul_zero (M₀ := ℝ≥0∞) (a := ε)]

Result:
x r : ℝ≥0∞
ε : ℝ≥0
hr : r < 1
h : ∀ (n : ℕ), x ≤ ↑ε * r ^ n
⊢ Tendsto (fun n => ↑ε * r ^ n) atTop (𝓝 (↑ε * 0))

Proof state:
x r : ℝ≥0∞
ε : ℝ≥0
hr : r < 1
h : ∀ (n : ℕ), x ≤ ↑ε * r ^ n
⊢ Tendsto (fun n => ↑ε * r ^ n) atTop (𝓝 (↑ε * 0))

Tactic:
exact Tendsto.const_mul (tendsto_pow_atTop_nhds_zero_of_lt_one hr) (Or.inr coe_ne_top)

Result:
no goals
-- Mathlib/Geometry/Manifold/IsManifold/ExtChartAt.lean
theorem extend_source : (f.extend I).source = f.source

Proof state:
𝕜 : Type u_1
E : Type u_2
M : Type u_3
H : Type u_4
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : TopologicalSpace H
inst✝ : TopologicalSpace M
f : PartialHomeomorph M H
I : ModelWithCorners 𝕜 E H
⊢ (f.extend I).source = f.source

Tactic:
rw [extend, PartialEquiv.trans_source, I.source_eq, preimage_univ, inter_univ]

Result:
no goals
-- Mathlib/Algebra/Order/Field/Basic.lean
lemma mul_le_of_forall_lt_of_nonneg {a b c : α} (ha : 0 ≤ a) (hc : 0 ≤ c)
    (h : ∀ a' ≥ 0, a' < a → ∀ b' ≥ 0, b' < b → a' * b' ≤ c) : a * b ≤ c

Proof state:
case inr
α : Type u_2
inst✝ : LinearOrderedField α
a b c : α
ha : 0 ≤ a
hc : 0 ≤ c
h : ∀ a' ≥ 0, a' < a → ∀ b' ≥ 0, b' < b → a' * b' ≤ c
d : α
d_ab : d < a * b
hd : 0 ≤ d
⊢ d ≤ c

Tactic:
obtain ⟨a', ha', d_ab⟩ := exists_lt_mul_left_of_nonneg ha hd d_ab

Result:
case inr.intro.intro
α : Type u_2
inst✝ : LinearOrderedField α
a b c : α
ha : 0 ≤ a
hc : 0 ≤ c
h : ∀ a' ≥ 0, a' < a → ∀ b' ≥ 0, b' < b → a' * b' ≤ c
d : α
d_ab✝ : d < a * b
hd : 0 ≤ d
a' : α
ha' : a' ∈ Set.Ico 0 a
d_ab : d < a' * b
⊢ d ≤ c

Proof state:
case inr.intro.intro.intro.intro
α : Type u_2
inst✝ : LinearOrderedField α
a b c : α
ha : 0 ≤ a
hc : 0 ≤ c
h : ∀ a' ≥ 0, a' < a → ∀ b' ≥ 0, b' < b → a' * b' ≤ c
d : α
d_ab✝¹ : d < a * b
hd : 0 ≤ d
a' : α
ha' : a' ∈ Set.Ico 0 a
d_ab✝ : d < a' * b
b' : α
hb' : b' ∈ Set.Ico 0 b
d_ab : d < a' * b'
⊢ d ≤ c

Tactic:
exact d_ab.le.trans (h a' ha'.1 ha'.2 b' hb'.1 hb'.2)

Result:
no goals

Proof state:
α : Type u_2
inst✝ : LinearOrderedField α
a b c : α
ha : 0 ≤ a
hc : 0 ≤ c
h : ∀ a' ≥ 0, a' < a → ∀ b' ≥ 0, b' < b → a' * b' ≤ c
⊢ a * b ≤ c

Tactic:
refine le_of_forall_lt_imp_le_of_dense fun d d_ab ↦ ?_

Result:
α : Type u_2
inst✝ : LinearOrderedField α
a b c : α
ha : 0 ≤ a
hc : 0 ≤ c
h : ∀ a' ≥ 0, a' < a → ∀ b' ≥ 0, b' < b → a' * b' ≤ c
d : α
d_ab : d < a * b
⊢ d ≤ c

Proof state:
case inr.intro.intro
α : Type u_2
inst✝ : LinearOrderedField α
a b c : α
ha : 0 ≤ a
hc : 0 ≤ c
h : ∀ a' ≥ 0, a' < a → ∀ b' ≥ 0, b' < b → a' * b' ≤ c
d : α
d_ab✝ : d < a * b
hd : 0 ≤ d
a' : α
ha' : a' ∈ Set.Ico 0 a
d_ab : d < a' * b
⊢ d ≤ c

Tactic:
obtain ⟨b', hb', d_ab⟩ := exists_lt_mul_right_of_nonneg ha'.1 hd d_ab

Result:
case inr.intro.intro.intro.intro
α : Type u_2
inst✝ : LinearOrderedField α
a b c : α
ha : 0 ≤ a
hc : 0 ≤ c
h : ∀ a' ≥ 0, a' < a → ∀ b' ≥ 0, b' < b → a' * b' ≤ c
d : α
d_ab✝¹ : d < a * b
hd : 0 ≤ d
a' : α
ha' : a' ∈ Set.Ico 0 a
d_ab✝ : d < a' * b
b' : α
hb' : b' ∈ Set.Ico 0 b
d_ab : d < a' * b'
⊢ d ≤ c

Proof state:
case inl
α : Type u_2
inst✝ : LinearOrderedField α
a b c : α
ha : 0 ≤ a
hc : 0 ≤ c
h : ∀ a' ≥ 0, a' < a → ∀ b' ≥ 0, b' < b → a' * b' ≤ c
d : α
d_ab : d < a * b
hd : d < 0
⊢ d ≤ c

Tactic:
exact hd.le.trans hc

Result:
no goals

Proof state:
α : Type u_2
inst✝ : LinearOrderedField α
a b c : α
ha : 0 ≤ a
hc : 0 ≤ c
h : ∀ a' ≥ 0, a' < a → ∀ b' ≥ 0, b' < b → a' * b' ≤ c
d : α
d_ab : d < a * b
⊢ d ≤ c

Tactic:
rcases lt_or_le d 0 with hd | hd

Result:
case inl
α : Type u_2
inst✝ : LinearOrderedField α
a b c : α
ha : 0 ≤ a
hc : 0 ≤ c
h : ∀ a' ≥ 0, a' < a → ∀ b' ≥ 0, b' < b → a' * b' ≤ c
d : α
d_ab : d < a * b
hd : d < 0
⊢ d ≤ c

case inr
α : Type u_2
inst✝ : LinearOrderedField α
a b c : α
ha : 0 ≤ a
hc : 0 ≤ c
h : ∀ a' ≥ 0, a' < a → ∀ b' ≥ 0, b' < b → a' * b' ≤ c
d : α
d_ab : d < a * b
hd : 0 ≤ d
⊢ d ≤ c
-- Mathlib/MeasureTheory/Constructions/Cylinders.lean
theorem union_cylinder_same (s : Finset ι) (S₁ : Set (∀ i : s, α i)) (S₂ : Set (∀ i : s, α i)) :
    cylinder s S₁ ∪ cylinder s S₂ = cylinder s (S₁ ∪ S₂)

Proof state:
ι : Type u_1
α : ι → Type u_2
s : Finset ι
S₁ S₂ : Set ((i : { x // x ∈ s }) → α ↑i)
⊢ cylinder (s ∪ s) (Finset.restrict₂ ⋯ ⁻¹' S₁ ∪ Finset.restrict₂ ⋯ ⁻¹' S₂) = cylinder s (S₁ ∪ S₂)

Tactic:
rfl

Result:
no goals

Proof state:
ι : Type u_1
α : ι → Type u_2
s : Finset ι
S₁ S₂ : Set ((i : { x // x ∈ s }) → α ↑i)
⊢ cylinder s S₁ ∪ cylinder s S₂ = cylinder s (S₁ ∪ S₂)

Tactic:
rw [union_cylinder]

Result:
ι : Type u_1
α : ι → Type u_2
s : Finset ι
S₁ S₂ : Set ((i : { x // x ∈ s }) → α ↑i)
⊢ cylinder (s ∪ s) (Finset.restrict₂ ⋯ ⁻¹' S₁ ∪ Finset.restrict₂ ⋯ ⁻¹' S₂) = cylinder s (S₁ ∪ S₂)

Proof state:
ι : Type u_1
α : ι → Type u_2
s : Finset ι
S₁ S₂ : Set ((i : { x // x ∈ s }) → α ↑i)
⊢ cylinder s S₁ ∪ cylinder s S₂ = cylinder s (S₁ ∪ S₂)

Tactic:
classical rw [union_cylinder]; rfl

Result:
no goals
-- Mathlib/Topology/Constructions.lean
theorem Topology.IsQuotientMap.restrictPreimage_isOpen {f : X → Y} (hf : IsQuotientMap f)
    {s : Set Y} (hs : IsOpen s) : IsQuotientMap (s.restrictPreimage f)

Proof state:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : IsQuotientMap f
s : Set Y
hs : IsOpen s
U : Set ↑s
⊢ IsOpen U ↔ IsOpen (s.restrictPreimage f ⁻¹' U)

Tactic:
rw [hs.isOpenEmbedding_subtypeVal.isOpen_iff_image_isOpen, ← hf.isOpen_preimage,
  (hs.preimage hf.continuous).isOpenEmbedding_subtypeVal.isOpen_iff_image_isOpen,
  image_val_preimage_restrictPreimage]

Result:
no goals

Proof state:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : IsQuotientMap f
s : Set Y
hs : IsOpen s
⊢ IsQuotientMap (s.restrictPreimage f)

Tactic:
refine isQuotientMap_iff.2 ⟨hf.surjective.restrictPreimage _, fun U ↦ ?_⟩

Result:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : IsQuotientMap f
s : Set Y
hs : IsOpen s
U : Set ↑s
⊢ IsOpen U ↔ IsOpen (s.restrictPreimage f ⁻¹' U)
-- Mathlib/AlgebraicGeometry/IdealSheaf.lean
@[simp]
lemma support_top : support (X := X) ⊤ = ∅

Proof state:
X : Scheme
⊢ ⊤.support = ∅

Tactic:
ext x

Result:
case h
X : Scheme
x : ↑↑X.toPresheafedSpace
⊢ x ∈ ⊤.support ↔ x ∈ ∅

Proof state:
case h.intro.intro.intro.intro.intro
X : Scheme
x : ↑↑X.toPresheafedSpace
U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace
hU : U ∈ X.affineOpens
hxU : x ∈ ↑U
⊢ x ∈ ⊤.support ↔ x ∈ ∅

Tactic:
simpa [support] using ⟨U, hU, hxU⟩

Result:
no goals

Proof state:
case h
X : Scheme
x : ↑↑X.toPresheafedSpace
⊢ x ∈ ⊤.support ↔ x ∈ ∅

Tactic:
obtain ⟨_, ⟨U, hU, rfl⟩, hxU, -⟩ :=
  (isBasis_affine_open X).exists_subset_of_mem_open (Set.mem_univ x) isOpen_univ

Result:
case h.intro.intro.intro.intro.intro
X : Scheme
x : ↑↑X.toPresheafedSpace
U : TopologicalSpace.Opens ↑↑X.toPresheafedSpace
hU : U ∈ X.affineOpens
hxU : x ∈ ↑U
⊢ x ∈ ⊤.support ↔ x ∈ ∅
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Bool.lean
theorem decide_iff_dist (p q : Prop) [dpq : Decidable (p ↔ q)] [dp : Decidable p] [dq : Decidable q] :
    decide (p ↔ q) = (decide p == decide q)

Proof state:
p q : Prop
dpq : Decidable (p ↔ q)
dp : Decidable p
dq : Decidable q
⊢ decide (p ↔ q) = (decide p == decide q)

Tactic:
cases dp with | _ p => simp [p]

Result:
no goals

Proof state:
case isTrue
p✝ q : Prop
dpq : Decidable (p✝ ↔ q)
dq : Decidable q
p : p✝
⊢ decide (p✝ ↔ q) = (decide p✝ == decide q)

Tactic:
simp [p]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Roots.lean
theorem card_roots_le_map [IsDomain A] [IsDomain B] {p : A[X]} {f : A →+* B} (h : p.map f ≠ 0) :
    Multiset.card p.roots ≤ Multiset.card (p.map f).roots

Proof state:
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : IsDomain A
inst✝ : IsDomain B
p : A[X]
f : A →+* B
h : map f p ≠ 0
⊢ p.roots.card ≤ (map f p).roots.card

Tactic:
rw [← p.roots.card_map f]

Result:
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : IsDomain A
inst✝ : IsDomain B
p : A[X]
f : A →+* B
h : map f p ≠ 0
⊢ (Multiset.map (⇑f) p.roots).card ≤ (map f p).roots.card

Proof state:
A : Type u_1
B : Type u_2
inst✝³ : CommRing A
inst✝² : CommRing B
inst✝¹ : IsDomain A
inst✝ : IsDomain B
p : A[X]
f : A →+* B
h : map f p ≠ 0
⊢ (Multiset.map (⇑f) p.roots).card ≤ (map f p).roots.card

Tactic:
exact Multiset.card_le_card (map_roots_le h)

Result:
no goals
-- Mathlib/Data/Finset/Sups.lean
theorem disjSups_disjSups_disjSups_comm : s ○ t ○ (u ○ v) = s ○ u ○ (t ○ v)

Proof state:
α : Type u_2
inst✝³ : DecidableEq α
inst✝² : DistribLattice α
inst✝¹ : OrderBot α
inst✝ : DecidableRel Disjoint
s t u v : Finset α
⊢ s ○ t ○ (u ○ v) = s ○ u ○ (t ○ v)

Tactic:
simp_rw [← disjSups_assoc, disjSups_right_comm]

Result:
no goals
-- Mathlib/Topology/StoneCech.lean
theorem preStoneCech_hom_ext {g₁ g₂ : PreStoneCech α → β} (h₁ : Continuous g₁) (h₂ : Continuous g₂)
    (h : g₁ ∘ preStoneCechUnit = g₂ ∘ preStoneCechUnit) : g₁ = g₂

Proof state:
α : Type u
inst✝² : TopologicalSpace α
β : Type v
inst✝¹ : TopologicalSpace β
inst✝ : T2Space β
g₁ g₂ : PreStoneCech α → β
h₁ : Continuous g₁
h₂ : Continuous g₂
h : g₁ ∘ preStoneCechUnit = g₂ ∘ preStoneCechUnit
⊢ g₁ = g₂

Tactic:
apply Continuous.ext_on denseRange_preStoneCechUnit h₁ h₂

Result:
α : Type u
inst✝² : TopologicalSpace α
β : Type v
inst✝¹ : TopologicalSpace β
inst✝ : T2Space β
g₁ g₂ : PreStoneCech α → β
h₁ : Continuous g₁
h₂ : Continuous g₂
h : g₁ ∘ preStoneCechUnit = g₂ ∘ preStoneCechUnit
⊢ EqOn g₁ g₂ (range preStoneCechUnit)

Proof state:
α : Type u
inst✝² : TopologicalSpace α
β : Type v
inst✝¹ : TopologicalSpace β
inst✝ : T2Space β
g₁ g₂ : PreStoneCech α → β
h₁ : Continuous g₁
h₂ : Continuous g₂
h : g₁ ∘ preStoneCechUnit = g₂ ∘ preStoneCechUnit
⊢ EqOn g₁ g₂ (range preStoneCechUnit)

Tactic:
rintro x ⟨x, rfl⟩

Result:
case intro
α : Type u
inst✝² : TopologicalSpace α
β : Type v
inst✝¹ : TopologicalSpace β
inst✝ : T2Space β
g₁ g₂ : PreStoneCech α → β
h₁ : Continuous g₁
h₂ : Continuous g₂
h : g₁ ∘ preStoneCechUnit = g₂ ∘ preStoneCechUnit
x : α
⊢ g₁ (preStoneCechUnit x) = g₂ (preStoneCechUnit x)

Proof state:
case intro
α : Type u
inst✝² : TopologicalSpace α
β : Type v
inst✝¹ : TopologicalSpace β
inst✝ : T2Space β
g₁ g₂ : PreStoneCech α → β
h₁ : Continuous g₁
h₂ : Continuous g₂
h : g₁ ∘ preStoneCechUnit = g₂ ∘ preStoneCechUnit
x : α
⊢ g₁ (preStoneCechUnit x) = g₂ (preStoneCechUnit x)

Tactic:
apply congr_fun h x

Result:
no goals
-- Mathlib/Tactic/Linarith/Lemmas.lean
theorem le_of_eq_of_le {α} [OrderedSemiring α] {a b : α} (ha : a = 0) (hb : b ≤ 0) : a + b ≤ 0

Proof state:
α : Type u_1
inst✝ : OrderedSemiring α
a b : α
ha : a = 0
hb : b ≤ 0
⊢ a + b ≤ 0

Tactic:
simp [*]

Result:
no goals
-- Mathlib/Data/Set/Image.lean
theorem eq_preimage_iff_image_eq {f : α → β} (hf : Bijective f) {s t} :
    s = f ⁻¹' t ↔ f '' s = t

Proof state:
α : Type u
β : Type v
f : α → β
hf : Bijective f
s : Set α
t : Set β
⊢ s = f ⁻¹' t ↔ f '' s = t

Tactic:
rw [← image_eq_image hf.1, hf.2.image_preimage]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Regularity/Uniform.lean
theorem IsUniform.mono {ε ε' : 𝕜} (hP : P.IsUniform G ε) (h : ε ≤ ε') : P.IsUniform G ε' :=
  ((Nat.cast_le.2 <| card_le_card <| P.nonUniforms_mono G h).trans hP).trans <| by gcongr

Proof state:
α : Type u_1
𝕜 : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : DecidableEq α
A : Finset α
P : Finpartition A
G : SimpleGraph α
inst✝ : DecidableRel G.Adj
ε ε' : 𝕜
hP : P.IsUniform G ε
h : ε ≤ ε'
⊢ ↑(#P.parts * (#P.parts - 1)) * ε ≤ ↑(#P.parts * (#P.parts - 1)) * ε'

Tactic:
gcongr

Result:
no goals
-- Mathlib/Algebra/Lie/CartanSubalgebra.lean
theorem LieIdeal.normalizer_eq_top {R : Type u} {L : Type v} [CommRing R] [LieRing L]
    [LieAlgebra R L] (I : LieIdeal R L) : (I : LieSubalgebra R L).normalizer = ⊤

Proof state:
case h
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I : LieIdeal R L
x : L
⊢ x ∈ (toLieSubalgebra R L I).normalizer ↔ x ∈ ⊤

Tactic:
simpa only [LieSubalgebra.mem_normalizer_iff, LieSubalgebra.mem_top, iff_true] using
  fun y hy => I.lie_mem hy

Result:
no goals

Proof state:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I : LieIdeal R L
⊢ (toLieSubalgebra R L I).normalizer = ⊤

Tactic:
ext x

Result:
case h
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I : LieIdeal R L
x : L
⊢ x ∈ (toLieSubalgebra R L I).normalizer ↔ x ∈ ⊤
-- Mathlib/Order/Filter/Finite.lean
theorem iInf_principal_finset {ι : Type w} (s : Finset ι) (f : ι → Set α) :
    ⨅ i ∈ s, 𝓟 (f i) = 𝓟 (⋂ i ∈ s, f i)

Proof state:
α : Type u
ι : Type w
s : Finset ι
f : ι → Set α
⊢ ⨅ i ∈ s, 𝓟 (f i) = 𝓟 (⋂ i ∈ s, f i)

Tactic:
induction' s using Finset.induction_on with i s _ hs

Result:
case empty
α : Type u
ι : Type w
f : ι → Set α
⊢ ⨅ i ∈ ∅, 𝓟 (f i) = 𝓟 (⋂ i ∈ ∅, f i)

case insert
α : Type u
ι : Type w
f : ι → Set α
i : ι
s : Finset ι
a✝ : i ∉ s
hs : ⨅ i ∈ s, 𝓟 (f i) = 𝓟 (⋂ i ∈ s, f i)
⊢ ⨅ i_1 ∈ insert i s, 𝓟 (f i_1) = 𝓟 (⋂ i_1 ∈ insert i s, f i_1)

Proof state:
case insert
α : Type u
ι : Type w
f : ι → Set α
i : ι
s : Finset ι
a✝ : i ∉ s
hs : ⨅ i ∈ s, 𝓟 (f i) = 𝓟 (⋂ i ∈ s, f i)
⊢ ⨅ i_1 ∈ insert i s, 𝓟 (f i_1) = 𝓟 (⋂ i_1 ∈ insert i s, f i_1)

Tactic:
rw [Finset.iInf_insert, Finset.set_biInter_insert, hs, inf_principal]

Result:
no goals

Proof state:
case empty
α : Type u
ι : Type w
f : ι → Set α
⊢ ⨅ i ∈ ∅, 𝓟 (f i) = 𝓟 (⋂ i ∈ ∅, f i)

Tactic:
simp

Result:
no goals
-- Mathlib/AlgebraicTopology/DoldKan/Projections.lean
theorem Q_f_0_eq (q : ℕ) : ((Q q).f 0 : X _⦋0⦌ ⟶ X _⦋0⦌) = 0

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
q : ℕ
⊢ (Q q).f 0 = 0

Tactic:
simp only [HomologicalComplex.sub_f_apply, HomologicalComplex.id_f, Q, P_f_0_eq, sub_self]

Result:
no goals
-- Mathlib/Data/Finset/Preimage.lean
theorem subset_map_iff {f : α ↪ β} {s : Finset β} {t : Finset α} :
    s ⊆ t.map f ↔ ∃ u ⊆ t, s = u.map f

Proof state:
α : Type u
β : Type v
f : α ↪ β
s : Finset β
t : Finset α
⊢ s ⊆ map f t ↔ ∃ u ⊆ t, s = map f u

Tactic:
simp_rw [map_eq_image, subset_image_iff, eq_comm]

Result:
no goals

Proof state:
α : Type u
β : Type v
f : α ↪ β
s : Finset β
t : Finset α
⊢ s ⊆ map f t ↔ ∃ u ⊆ t, s = map f u

Tactic:
classical
simp_rw [map_eq_image, subset_image_iff, eq_comm]

Result:
no goals
-- Mathlib/LinearAlgebra/Ray.lean
theorem _root_.Function.Injective.sameRay_map_iff
    {F : Type*} [FunLike F M N] [LinearMapClass F R M N]
    {f : F} (hf : Function.Injective f) :
    SameRay R (f x) (f y) ↔ SameRay R x y

Proof state:
R : Type u_1
inst✝⁶ : StrictOrderedCommSemiring R
M : Type u_2
inst✝⁵ : AddCommMonoid M
inst✝⁴ : Module R M
N : Type u_3
inst✝³ : AddCommMonoid N
inst✝² : Module R N
x y : M
F : Type u_6
inst✝¹ : FunLike F M N
inst✝ : LinearMapClass F R M N
f : F
hf : Function.Injective ⇑f
⊢ SameRay R (f x) (f y) ↔ SameRay R x y

Tactic:
simp only [SameRay, map_zero, ← hf.eq_iff, map_smul]

Result:
no goals
-- Mathlib/Algebra/BigOperators/Intervals.lean
theorem sum_range_id_mul_two (n : ℕ) : (∑ i ∈ range n, i) * 2 = n * (n - 1) :=
  calc
    (∑ i ∈ range n, i) * 2 = (∑ i ∈ range n, i) + ∑ i ∈ range n, (n - 1 - i)

Proof state:
n : ℕ
⊢ ∑ x ∈ range n, (n - 1) = n * (n - 1)

Tactic:
rw [sum_const, card_range, Nat.nsmul_eq_mul]

Result:
no goals

Proof state:
n : ℕ
⊢ (∑ i ∈ range n, i) * 2 = ∑ i ∈ range n, i + ∑ i ∈ range n, (n - 1 - i)

Tactic:
rw [sum_range_reflect (fun i => i) n, mul_two]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Path.lean
theorem connectedComponentEquiv_refl :
    (Iso.refl : G ≃g G).connectedComponentEquiv = Equiv.refl _

Proof state:
V : Type u
G : SimpleGraph V
⊢ refl.connectedComponentEquiv = Equiv.refl G.ConnectedComponent

Tactic:
ext ⟨v⟩

Result:
case H.mk
V : Type u
G : SimpleGraph V
x✝ : G.ConnectedComponent
v : V
⊢ refl.connectedComponentEquiv (Quot.mk G.Reachable v) = (Equiv.refl G.ConnectedComponent) (Quot.mk G.Reachable v)

Proof state:
case H.mk
V : Type u
G : SimpleGraph V
x✝ : G.ConnectedComponent
v : V
⊢ refl.connectedComponentEquiv (Quot.mk G.Reachable v) = (Equiv.refl G.ConnectedComponent) (Quot.mk G.Reachable v)

Tactic:
rfl

Result:
no goals
-- Mathlib/RingTheory/UniqueFactorizationDomain/FactorSet.lean
theorem factors_self [Nontrivial α] {p : Associates α} (hp : Irreducible p) :
    p.factors = WithTop.some {⟨p, hp⟩} :=
  eq_of_prod_eq_prod
    (by rw [factors_prod, FactorSet.prod.eq_def]; dsimp; rw [prod_singleton])

Proof state:
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : Nontrivial α
p : Associates α
hp : Irreducible p
⊢ p = {p}.prod

Tactic:
rw [prod_singleton]

Result:
no goals

Proof state:
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : Nontrivial α
p : Associates α
hp : Irreducible p
⊢ p =
    match ↑{⟨p, hp⟩} with
    | none => 0
    | some s => (Multiset.map Subtype.val s).prod

Tactic:
dsimp

Result:
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : Nontrivial α
p : Associates α
hp : Irreducible p
⊢ p = {p}.prod

Proof state:
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : Nontrivial α
p : Associates α
hp : Irreducible p
⊢ p.factors.prod = FactorSet.prod ↑{⟨p, hp⟩}

Tactic:
rw [factors_prod, FactorSet.prod.eq_def]

Result:
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : UniqueFactorizationMonoid α
inst✝ : Nontrivial α
p : Associates α
hp : Irreducible p
⊢ p =
    match ↑{⟨p, hp⟩} with
    | none => 0
    | some s => (Multiset.map Subtype.val s).prod
-- Mathlib/Analysis/InnerProductSpace/Basic.lean
theorem re_inner_eq_norm_mul_self_add_norm_mul_self_sub_norm_sub_mul_self_div_two (x y : E) :
    re ⟪x, y⟫ = (‖x‖ * ‖x‖ + ‖y‖ * ‖y‖ - ‖x - y‖ * ‖x - y‖) / 2

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y : E
⊢ re ⟪x, y⟫_𝕜 = (‖x‖ * ‖x‖ + ‖y‖ * ‖y‖ - ‖x - y‖ * ‖x - y‖) / 2

Tactic:
rw [@norm_sub_mul_self 𝕜]

Result:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y : E
⊢ re ⟪x, y⟫_𝕜 = (‖x‖ * ‖x‖ + ‖y‖ * ‖y‖ - (‖x‖ * ‖x‖ - 2 * re ⟪x, y⟫_𝕜 + ‖y‖ * ‖y‖)) / 2

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : RCLike 𝕜
inst✝¹ : SeminormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
x y : E
⊢ re ⟪x, y⟫_𝕜 = (‖x‖ * ‖x‖ + ‖y‖ * ‖y‖ - (‖x‖ * ‖x‖ - 2 * re ⟪x, y⟫_𝕜 + ‖y‖ * ‖y‖)) / 2

Tactic:
ring

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/MapIdx.lean
theorem mapFinIdx_singleton {a : α} {f : (i : Nat) → α → (h : i < 1) → β} :
    #[a].mapFinIdx f = #[f 0 a (by simp)]

Proof state:
α : Type ?u.58212
β : Type ?u.58218
a : α
f : (i : Nat) → α → i < 1 → β
⊢ 0 < 1

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
a : α
f : (i : Nat) → α → i < 1 → β
⊢ #[a].mapFinIdx f = #[f 0 a ⋯]

Tactic:
simp

Result:
no goals
-- Mathlib/MeasureTheory/Measure/MeasureSpace.lean
theorem le_intro (h : ∀ s, MeasurableSet s → s.Nonempty → μ₁ s ≤ μ₂ s) : μ₁ ≤ μ₂ :=
  le_iff.2 fun s hs ↦ s.eq_empty_or_nonempty.elim (by rintro rfl; simp) (h s hs)

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ₁ μ₂ : Measure α
h : ∀ (s : Set α), MeasurableSet s → s.Nonempty → μ₁ s ≤ μ₂ s
s : Set α
hs : MeasurableSet s
⊢ s = ∅ → μ₁ s ≤ μ₂ s

Tactic:
rintro rfl

Result:
α : Type u_1
m0 : MeasurableSpace α
μ₁ μ₂ : Measure α
h : ∀ (s : Set α), MeasurableSet s → s.Nonempty → μ₁ s ≤ μ₂ s
hs : MeasurableSet ∅
⊢ μ₁ ∅ ≤ μ₂ ∅

Proof state:
α : Type u_1
m0 : MeasurableSpace α
μ₁ μ₂ : Measure α
h : ∀ (s : Set α), MeasurableSet s → s.Nonempty → μ₁ s ≤ μ₂ s
hs : MeasurableSet ∅
⊢ μ₁ ∅ ≤ μ₂ ∅

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/GroupWithZero/Commute.lean
theorem mul_inverse_rev' {a b : M₀} (h : Commute a b) :
    inverse (a * b) = inverse b * inverse a

Proof state:
M₀ : Type u_1
inst✝ : MonoidWithZero M₀
a b : M₀
h : Commute a b
⊢ inverse (a * b) = inverse b * inverse a

Tactic:
by_cases hab : IsUnit (a * b)

Result:
case pos
M₀ : Type u_1
inst✝ : MonoidWithZero M₀
a b : M₀
h : Commute a b
hab : IsUnit (a * b)
⊢ inverse (a * b) = inverse b * inverse a

case neg
M₀ : Type u_1
inst✝ : MonoidWithZero M₀
a b : M₀
h : Commute a b
hab : ¬IsUnit (a * b)
⊢ inverse (a * b) = inverse b * inverse a

Proof state:
case neg.inl
M₀ : Type u_1
inst✝ : MonoidWithZero M₀
a b : M₀
h : Commute a b
hab : ¬IsUnit (a * b)
ha : ¬IsUnit a
⊢ inverse (a * b) = inverse b * inverse a

Tactic:
rw [inverse_non_unit _ hab, inverse_non_unit _ ha, mul_zero]

Result:
no goals

Proof state:
case pos.intro.intro.intro
M₀ : Type u_1
inst✝ : MonoidWithZero M₀
a b : M₀ˣ
h : Commute ↑a ↑b
hab : IsUnit (↑a * ↑b)
⊢ inverse (↑a * ↑b) = inverse ↑b * inverse ↑a

Tactic:
rw [← Units.val_mul, inverse_unit, inverse_unit, inverse_unit, ← Units.val_mul, mul_inv_rev]

Result:
no goals

Proof state:
case neg
M₀ : Type u_1
inst✝ : MonoidWithZero M₀
a b : M₀
h : Commute a b
hab : ¬IsUnit (a * b)
⊢ inverse (a * b) = inverse b * inverse a

Tactic:
obtain ha | hb := not_and_or.mp (mt h.isUnit_mul_iff.mpr hab)

Result:
case neg.inl
M₀ : Type u_1
inst✝ : MonoidWithZero M₀
a b : M₀
h : Commute a b
hab : ¬IsUnit (a * b)
ha : ¬IsUnit a
⊢ inverse (a * b) = inverse b * inverse a

case neg.inr
M₀ : Type u_1
inst✝ : MonoidWithZero M₀
a b : M₀
h : Commute a b
hab : ¬IsUnit (a * b)
hb : ¬IsUnit b
⊢ inverse (a * b) = inverse b * inverse a

Proof state:
case pos
M₀ : Type u_1
inst✝ : MonoidWithZero M₀
a b : M₀
h : Commute a b
hab : IsUnit (a * b)
⊢ inverse (a * b) = inverse b * inverse a

Tactic:
obtain ⟨⟨a, rfl⟩, b, rfl⟩ := h.isUnit_mul_iff.mp hab

Result:
case pos.intro.intro.intro
M₀ : Type u_1
inst✝ : MonoidWithZero M₀
a b : M₀ˣ
h : Commute ↑a ↑b
hab : IsUnit (↑a * ↑b)
⊢ inverse (↑a * ↑b) = inverse ↑b * inverse ↑a

Proof state:
case neg.inr
M₀ : Type u_1
inst✝ : MonoidWithZero M₀
a b : M₀
h : Commute a b
hab : ¬IsUnit (a * b)
hb : ¬IsUnit b
⊢ inverse (a * b) = inverse b * inverse a

Tactic:
rw [inverse_non_unit _ hab, inverse_non_unit _ hb, zero_mul]

Result:
no goals
-- Mathlib/Data/Set/NAry.lean
theorem image2_subset (hs : s ⊆ s') (ht : t ⊆ t') : image2 f s t ⊆ image2 f s' t'

Proof state:
α : Type u_1
β : Type u_3
γ : Type u_5
f : α → β → γ
s s' : Set α
t t' : Set β
hs : s ⊆ s'
ht : t ⊆ t'
⊢ image2 f s t ⊆ image2 f s' t'

Tactic:
rintro _ ⟨a, ha, b, hb, rfl⟩

Result:
case intro.intro.intro.intro
α : Type u_1
β : Type u_3
γ : Type u_5
f : α → β → γ
s s' : Set α
t t' : Set β
hs : s ⊆ s'
ht : t ⊆ t'
a : α
ha : a ∈ s
b : β
hb : b ∈ t
⊢ f a b ∈ image2 f s' t'

Proof state:
case intro.intro.intro.intro
α : Type u_1
β : Type u_3
γ : Type u_5
f : α → β → γ
s s' : Set α
t t' : Set β
hs : s ⊆ s'
ht : t ⊆ t'
a : α
ha : a ∈ s
b : β
hb : b ∈ t
⊢ f a b ∈ image2 f s' t'

Tactic:
exact mem_image2_of_mem (hs ha) (ht hb)

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Oriented/Basic.lean
theorem two_zsmul_oangle_neg_self_left (x : V) : (2 : ℤ) • o.oangle (-x) x = 0

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

Tactic:
by_cases hx : x = 0 <;> simp [hx]

Result:
no goals