harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/CategoryTheory/Sites/EqualizerSheafCondition.lean
theorem w : forkMap P X π ≫ firstMap P X π = forkMap P X π ≫ secondMap P X π

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type w
B : C
I : Type
X : I → C
π : (i : I) → X i ⟶ B
inst✝ : (Presieve.ofArrows X π).hasPullbacks
⊢ forkMap P X π ≫ firstMap P X π = forkMap P X π ≫ secondMap P X π

Tactic:
ext x ij

Result:
case h.h
C : Type u
inst✝¹ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type w
B : C
I : Type
X : I → C
π : (i : I) → X i ⟶ B
inst✝ : (Presieve.ofArrows X π).hasPullbacks
x : P.obj (op B)
ij : I × I
⊢ Pi.π (fun ij => P.obj (op (Limits.pullback (π ij.1) (π ij.2)))) ij ((forkMap P X π ≫ firstMap P X π) x) =
    Pi.π (fun ij => P.obj (op (Limits.pullback (π ij.1) (π ij.2)))) ij ((forkMap P X π ≫ secondMap P X π) x)

Proof state:
case h.h
C : Type u
inst✝¹ : Category.{v, u} C
P : Cᵒᵖ ⥤ Type w
B : C
I : Type
X : I → C
π : (i : I) → X i ⟶ B
inst✝ : (Presieve.ofArrows X π).hasPullbacks
x : P.obj (op B)
ij : I × I
⊢ Pi.π (fun ij => P.obj (op (Limits.pullback (π ij.1) (π ij.2)))) ij ((forkMap P X π ≫ firstMap P X π) x) =
    Pi.π (fun ij => P.obj (op (Limits.pullback (π ij.1) (π ij.2)))) ij ((forkMap P X π ≫ secondMap P X π) x)

Tactic:
simp only [firstMap, secondMap, forkMap, types_comp_apply, Types.pi_lift_π_apply,
  ← FunctorToTypes.map_comp_apply, ← op_comp, pullback.condition]

Result:
no goals
-- Mathlib/Topology/ContinuousMap/Bounded/Basic.lean
theorem dist_lt_of_nonempty_compact [Nonempty α] [CompactSpace α]
    (w : ∀ x : α, dist (f x) (g x) < C) : dist f g < C

Proof state:
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : PseudoMetricSpace β
f g : α →ᵇ β
C : ℝ
inst✝¹ : Nonempty α
inst✝ : CompactSpace α
w : ∀ (x : α), dist (f x) (g x) < C
c : Continuous fun x => dist (f x) (g x)
⊢ dist f g < C

Tactic:
obtain ⟨x, -, le⟩ :=
  IsCompact.exists_isMaxOn isCompact_univ Set.univ_nonempty (Continuous.continuousOn c)

Result:
case intro.intro
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : PseudoMetricSpace β
f g : α →ᵇ β
C : ℝ
inst✝¹ : Nonempty α
inst✝ : CompactSpace α
w : ∀ (x : α), dist (f x) (g x) < C
c : Continuous fun x => dist (f x) (g x)
x : α
le : IsMaxOn (fun x => dist (f x) (g x)) univ x
⊢ dist f g < C

Proof state:
case intro.intro
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : PseudoMetricSpace β
f g : α →ᵇ β
C : ℝ
inst✝¹ : Nonempty α
inst✝ : CompactSpace α
w : ∀ (x : α), dist (f x) (g x) < C
c : Continuous fun x => dist (f x) (g x)
x : α
le : IsMaxOn (fun x => dist (f x) (g x)) univ x
⊢ dist f g < C

Tactic:
exact lt_of_le_of_lt (dist_le_iff_of_nonempty.mpr fun y => le trivial) (w x)

Result:
no goals

Proof state:
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : PseudoMetricSpace β
f g : α →ᵇ β
C : ℝ
inst✝¹ : Nonempty α
inst✝ : CompactSpace α
w : ∀ (x : α), dist (f x) (g x) < C
⊢ dist f g < C

Tactic:
have c : Continuous fun x => dist (f x) (g x) := by continuity

Result:
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : PseudoMetricSpace β
f g : α →ᵇ β
C : ℝ
inst✝¹ : Nonempty α
inst✝ : CompactSpace α
w : ∀ (x : α), dist (f x) (g x) < C
c : Continuous fun x => dist (f x) (g x)
⊢ dist f g < C

Proof state:
α : Type u
β : Type v
inst✝³ : TopologicalSpace α
inst✝² : PseudoMetricSpace β
f g : α →ᵇ β
C : ℝ
inst✝¹ : Nonempty α
inst✝ : CompactSpace α
w : ∀ (x : α), dist (f x) (g x) < C
⊢ Continuous fun x => dist (f x) (g x)

Tactic:
continuity

Result:
no goals
-- Mathlib/NumberTheory/Padics/PadicVal/Defs.lean
theorem eq_zero_iff {n : ℕ} : padicValNat p n = 0 ↔ p = 1 ∨ n = 0 ∨ ¬p ∣ n

Proof state:
p n : ℕ
⊢ padicValNat p n = 0 ↔ p = 1 ∨ n = 0 ∨ ¬p ∣ n

Tactic:
simp only [padicValNat, ne_eq, pos_iff_ne_zero, dite_eq_right_iff, find_eq_zero, zero_add,
  pow_one, and_imp, ← or_iff_not_imp_left]

Result:
no goals
-- Mathlib/Algebra/Group/Fin/Tuple.lean
@[simp] lemma neg_cons (x : α) (v : Fin n → α) : -vecCons x v = vecCons (-x) (-v)

Proof state:
case h
α : Type u_1
n : ℕ
inst✝ : Neg α
x : α
v : Fin n → α
i : Fin n.succ
⊢ (-vecCons x v) i = vecCons (-x) (-v) i

Tactic:
refine i.cases ?_ ?_ <;> simp

Result:
no goals

Proof state:
α : Type u_1
n : ℕ
inst✝ : Neg α
x : α
v : Fin n → α
⊢ -vecCons x v = vecCons (-x) (-v)

Tactic:
ext i

Result:
case h
α : Type u_1
n : ℕ
inst✝ : Neg α
x : α
v : Fin n → α
i : Fin n.succ
⊢ (-vecCons x v) i = vecCons (-x) (-v) i
-- Mathlib/NumberTheory/ModularForms/CongruenceSubgroups.lean
theorem Gamma_is_cong_sub (N : ℕ+) : IsCongruenceSubgroup (Gamma N) :=
  ⟨N, by simp only [le_refl]⟩

Proof state:
N : ℕ+
⊢ Γ(↑N) ≤ Γ(↑N)

Tactic:
simp only [le_refl]

Result:
no goals
-- Mathlib/Data/Finsupp/Multiset.lean
theorem toFinsupp_union (s t : Multiset α) : toFinsupp (s ∪ t) = toFinsupp s ⊔ toFinsupp t

Proof state:
case h
α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
a✝ : α
⊢ (toFinsupp (s ∪ t)) a✝ = (toFinsupp s ⊔ toFinsupp t) a✝

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
⊢ toFinsupp (s ∪ t) = toFinsupp s ⊔ toFinsupp t

Tactic:
ext

Result:
case h
α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
a✝ : α
⊢ (toFinsupp (s ∪ t)) a✝ = (toFinsupp s ⊔ toFinsupp t) a✝
-- Mathlib/LinearAlgebra/RootSystem/Hom.lean
@[simp]
lemma comp_assoc {ι₁ M₁ N₁ ι₂ M₂ N₂ ι₃ M₃ N₃ : Type*} [AddCommGroup M₁] [Module R M₁]
    [AddCommGroup N₁] [Module R N₁] [AddCommGroup M₂] [Module R M₂] [AddCommGroup N₂] [Module R N₂]
    [AddCommGroup M₃] [Module R M₃] [AddCommGroup N₃] [Module R N₃] {P : RootPairing ι R M N}
    {P₁ : RootPairing ι₁ R M₁ N₁} {P₂ : RootPairing ι₂ R M₂ N₂} {P₃ : RootPairing ι₃ R M₃ N₃}
    (h : Hom P₂ P₃) (g : Hom P₁ P₂) (f : Hom P P₁) :
    comp (comp h g) f = comp h (comp g f)

Proof state:
ι : Type u_1
R : Type u_2
M : Type u_3
N : Type u_4
inst✝¹⁶ : CommRing R
inst✝¹⁵ : AddCommGroup M
inst✝¹⁴ : Module R M
inst✝¹³ : AddCommGroup N
inst✝¹² : Module R N
ι₁ : Type u_5
M₁ : Type u_6
N₁ : Type u_7
ι₂ : Type u_8
M₂ : Type u_9
N₂ : Type u_10
ι₃ : Type u_11
M₃ : Type u_12
N₃ : Type u_13
inst✝¹¹ : AddCommGroup M₁
inst✝¹⁰ : Module R M₁
inst✝⁹ : AddCommGroup N₁
inst✝⁸ : Module R N₁
inst✝⁷ : AddCommGroup M₂
inst✝⁶ : Module R M₂
inst✝⁵ : AddCommGroup N₂
inst✝⁴ : Module R N₂
inst✝³ : AddCommGroup M₃
inst✝² : Module R M₃
inst✝¹ : AddCommGroup N₃
inst✝ : Module R N₃
P : RootPairing ι R M N
P₁ : RootPairing ι₁ R M₁ N₁
P₂ : RootPairing ι₂ R M₂ N₂
P₃ : RootPairing ι₃ R M₃ N₃
h : P₂.Hom P₃
g : P₁.Hom P₂
f : P.Hom P₁
⊢ (h.comp g).comp f = h.comp (g.comp f)

Tactic:
ext <;> simp

Result:
no goals
-- Mathlib/CategoryTheory/SmallObject/Iteration/Basic.lean
lemma mapEq_refl (k : K) (hk : k ≤ x) (h : F.obj ⟨k, hk⟩ = G.obj ⟨k, hk⟩) :
    MapEq F G k k (by simp) hk

Proof state:
C : Type u
inst✝⁶ : Category.{v, u} C
J : Type w
Φ : SuccStruct C
inst✝⁵ : LinearOrder J
inst✝⁴ : SuccOrder J
inst✝³ : OrderBot J
inst✝² : HasIterationOfShape J C
inst✝¹ : WellFoundedLT J
j : J
K : Type w
inst✝ : LinearOrder K
x : K
F G : ↑(Set.Iic x) ⥤ C
k : K
hk : k ≤ x
h : F.obj ⟨k, hk⟩ = G.obj ⟨k, hk⟩
⊢ k ≤ k

Tactic:
simp

Result:
no goals

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
K : Type w
inst✝ : LinearOrder K
x : K
F G : ↑(Set.Iic x) ⥤ C
k : K
hk : k ≤ x
h : F.obj ⟨k, hk⟩ = G.obj ⟨k, hk⟩
⊢ MapEq F G k k ⋯ hk

Tactic:
rw [MapEq, arrowMap_refl, arrowMap_refl, h]

Result:
no goals
-- Mathlib/Topology/MetricSpace/Pseudo/Defs.lean
theorem dense_iff_iUnion_ball (s : Set α) : Dense s ↔ ∀ r > 0, ⋃ c ∈ s, ball c r = univ

Proof state:
α : Type u
inst✝ : PseudoMetricSpace α
s : Set α
⊢ Dense s ↔ ∀ r > 0, ⋃ c ∈ s, ball c r = univ

Tactic:
simp_rw [eq_univ_iff_forall, mem_iUnion, exists_prop, mem_ball, Dense, mem_closure_iff,
  forall_comm (α := α)]

Result:
no goals
-- Mathlib/GroupTheory/Complement.lean
theorem inv_mul_toLeftFun_mem (hS : IsComplement S H) (g : G) :
    g⁻¹ * toLeftFun hS g ∈ H :=
  (congr_arg (· ∈ H) (by rw [mul_inv_rev, inv_inv])).mp (H.inv_mem (inv_toLeftFun_mul_mem hS g))

Proof state:
G : Type u_1
inst✝ : Group G
H : Subgroup G
S : Set G
hS : IsComplement S ↑H
g : G
⊢ ((↑(hS.toLeftFun g))⁻¹ * g)⁻¹ = g⁻¹ * ↑(hS.toLeftFun g)

Tactic:
rw [mul_inv_rev, inv_inv]

Result:
no goals
-- Mathlib/Algebra/ModEq.lean
theorem add_modEq_left : a + b ≡ a [PMOD p] ↔ b ≡ 0 [PMOD p]

Proof state:
α : Type u_1
inst✝ : AddCommGroup α
p a b : α
⊢ a + b ≡ a [PMOD p] ↔ b ≡ 0 [PMOD p]

Tactic:
simp [← modEq_sub_iff_add_modEq']

Result:
no goals
-- Mathlib/CategoryTheory/NatIso.lean
@[reassoc (attr := simp)]
lemma inv_hom_id_app_app {F G : C ⥤ D ⥤ E} (e : F ≅ G) (X₁ : C) (X₂ : D) :
    (e.inv.app X₁).app X₂ ≫ (e.hom.app X₁).app X₂ = 𝟙 _

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
E : Type u₃
inst✝ : Category.{v₃, u₃} E
F G : C ⥤ D ⥤ E
e : F ≅ G
X₁ : C
X₂ : D
⊢ (e.inv.app X₁).app X₂ ≫ (e.hom.app X₁).app X₂ = 𝟙 ((G.obj X₁).obj X₂)

Tactic:
rw [← NatTrans.comp_app, Iso.inv_hom_id_app, NatTrans.id_app]

Result:
no goals
-- Mathlib/Data/Set/Prod.lean
theorem mk_preimage_prod_left_fn_eq_if [DecidablePred (· ∈ t)] (f : γ → α) :
    (fun a => (f a, b)) ⁻¹' s ×ˢ t = if b ∈ t then f ⁻¹' s else ∅

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
s : Set α
t : Set β
b : β
inst✝ : DecidablePred fun x => x ∈ t
f : γ → α
⊢ (fun a => (f a, b)) ⁻¹' s ×ˢ t = if b ∈ t then f ⁻¹' s else ∅

Tactic:
rw [← mk_preimage_prod_left_eq_if, prod_preimage_left, preimage_preimage]

Result:
no goals
-- Mathlib/Data/Nat/PrimeFin.lean
/-- The only prime divisor of positive prime power `p^k` is `p` itself -/
lemma primeFactors_prime_pow (hk : k ≠ 0) (hp : Prime p) :
    (p ^ k).primeFactors = {p}

Proof state:
k p : ℕ
hk : k ≠ 0
hp : Prime p
⊢ (p ^ k).primeFactors = {p}

Tactic:
simp [primeFactors_pow p hk, hp]

Result:
no goals
-- Mathlib/Algebra/Group/Nat/Even.lean
lemma not_even_iff : ¬ Even n ↔ n % 2 = 1

Proof state:
n : ℕ
⊢ ¬Even n ↔ n % 2 = 1

Tactic:
rw [even_iff, mod_two_not_eq_zero]

Result:
no goals
-- Mathlib/LinearAlgebra/LinearPMap.lean
theorem toLinearPMap_range (g : Submodule R (E × F))
    (hg : ∀ (x : E × F) (_hx : x ∈ g) (_hx' : x.fst = 0), x.snd = 0) :
    LinearMap.range g.toLinearPMap.toFun = g.map (LinearMap.snd R E F)

Proof state:
R : Type u_1
inst✝⁴ : Ring R
E : Type u_2
inst✝³ : AddCommGroup E
inst✝² : Module R E
F : Type u_3
inst✝¹ : AddCommGroup F
inst✝ : Module R F
g : Submodule R (E × F)
hg : ∀ x ∈ g, x.1 = 0 → x.2 = 0
⊢ LinearMap.range g.toLinearPMap.toFun = map (LinearMap.snd R E F) g

Tactic:
rwa [← LinearPMap.graph_map_snd_eq_range, toLinearPMap_graph_eq]

Result:
no goals
-- Mathlib/CategoryTheory/Comma/StructuredArrow/Basic.lean
theorem hom_ext (h : IsUniversal f) {c : C} {η η' : f.right ⟶ c}
    (w : f.hom ≫ T.map η = f.hom ≫ T.map η') : η = η'

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
D : Type u₂
inst✝ : Category.{v₂, u₂} D
S : D
T : C ⥤ D
f : StructuredArrow S T
h : f.IsUniversal
c : C
η η' : f.right ⟶ c
w : f.hom ≫ T.map η = f.hom ≫ T.map η'
⊢ η = η'

Tactic:
rw [h.hom_desc η, h.hom_desc η', w]

Result:
no goals
-- Mathlib/Algebra/Ring/Periodic.lean
theorem Antiperiodic.sub_const [AddCommGroup α] [Neg β] (h : Antiperiodic f c) (a : α) :
    Antiperiodic (fun x => f (x - a)) c

Proof state:
α : Type u_1
β : Type u_2
f : α → β
c : α
inst✝¹ : AddCommGroup α
inst✝ : Neg β
h : Antiperiodic f c
a : α
⊢ Antiperiodic (fun x => f (x - a)) c

Tactic:
simpa only [sub_eq_add_neg] using h.add_const (-a)

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/NNReal.lean
/-- Variant of `NNReal.rpow_add'` that avoids having to prove `y + z = w` twice. -/
lemma rpow_of_add_eq (x : ℝ≥0) (hw : w ≠ 0) (h : y + z = w) : x ^ w = x ^ y * x ^ z

Proof state:
w y z : ℝ
x : ℝ≥0
hw : w ≠ 0
h : y + z = w
⊢ x ^ w = x ^ y * x ^ z

Tactic:
rw [← h, rpow_add']

Result:
case h
w y z : ℝ
x : ℝ≥0
hw : w ≠ 0
h : y + z = w
⊢ y + z ≠ 0

Proof state:
case h
w y z : ℝ
x : ℝ≥0
hw : w ≠ 0
h : y + z = w
⊢ y + z ≠ 0

Tactic:
rwa [h]

Result:
no goals
-- Mathlib/Probability/Distributions/Gaussian.lean
lemma gaussianReal_apply (μ : ℝ) {v : ℝ≥0} (hv : v ≠ 0) (s : Set ℝ) :
    gaussianReal μ v s = ∫⁻ x in s, gaussianPDF μ v x

Proof state:
μ : ℝ
v : ℝ≥0
hv : v ≠ 0
s : Set ℝ
⊢ (gaussianReal μ v) s = ∫⁻ (x : ℝ) in s, gaussianPDF μ v x

Tactic:
rw [gaussianReal_of_var_ne_zero _ hv, withDensity_apply' _ s]

Result:
no goals
-- Mathlib/Algebra/BigOperators/Group/Multiset/Basic.lean
theorem prod_hom₂_ne_zero [CommMonoid γ] {s : Multiset ι} (hs : s ≠ 0) (f : α → β → γ)
    (hf : ∀ a b c d, f (a * b) (c * d) = f a c * f b d) (f₁ : ι → α) (f₂ : ι → β) :
    (s.map fun i => f (f₁ i) (f₂ i)).prod = f (s.map f₁).prod (s.map f₂).prod

Proof state:
case h
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_6
inst✝² : CommMonoid α
inst✝¹ : CommMonoid β
inst✝ : CommMonoid γ
f : α → β → γ
hf : ∀ (a b : α) (c d : β), f (a * b) (c * d) = f a c * f b d
f₁ : ι → α
f₂ : ι → β
a✝ : List ι
hs : ⟦a✝⟧ ≠ 0
⊢ (map (fun i => f (f₁ i) (f₂ i)) ⟦a✝⟧).prod = f (map f₁ ⟦a✝⟧).prod (map f₂ ⟦a✝⟧).prod

Tactic:
aesop (add simp List.prod_hom₂_nonempty)

Result:
no goals

Proof state:
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_6
inst✝² : CommMonoid α
inst✝¹ : CommMonoid β
inst✝ : CommMonoid γ
s : Multiset ι
hs : s ≠ 0
f : α → β → γ
hf : ∀ (a b : α) (c d : β), f (a * b) (c * d) = f a c * f b d
f₁ : ι → α
f₂ : ι → β
⊢ (map (fun i => f (f₁ i) (f₂ i)) s).prod = f (map f₁ s).prod (map f₂ s).prod

Tactic:
induction s using Quotient.inductionOn

Result:
case h
ι : Type u_2
α : Type u_3
β : Type u_4
γ : Type u_6
inst✝² : CommMonoid α
inst✝¹ : CommMonoid β
inst✝ : CommMonoid γ
f : α → β → γ
hf : ∀ (a b : α) (c d : β), f (a * b) (c * d) = f a c * f b d
f₁ : ι → α
f₂ : ι → β
a✝ : List ι
hs : ⟦a✝⟧ ≠ 0
⊢ (map (fun i => f (f₁ i) (f₂ i)) ⟦a✝⟧).prod = f (map f₁ ⟦a✝⟧).prod (map f₂ ⟦a✝⟧).prod
-- Mathlib/Order/Interval/Set/UnorderedInterval.lean
lemma eq_of_mem_uIcc_of_mem_uIcc' : b ∈ [[a, c]] → c ∈ [[a, b]] → b = c

Proof state:
α : Type u_1
inst✝ : DistribLattice α
a b c : α
⊢ b ∈ [[a, c]] → c ∈ [[a, b]] → b = c

Tactic:
simpa only [uIcc_comm a] using eq_of_mem_uIcc_of_mem_uIcc

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/RawLemmas.lean
theorem get?_insert [EquivBEq α] [LawfulHashable α] (h : m.1.WF) {k a : α} {v : β} :
    get? (m.insert k v) a = if k == a then some v else get? m a

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
β : Type v
m : Raw₀ α fun x => β
inst✝¹ : EquivBEq α
inst✝ : LawfulHashable α
h : m.val.WF
k a : α
v : β
⊢ get? (m.insert k v) a = if (k == a) = true then some v else get? m a

Tactic:
simp_to_model [insert] using List.getValue?_insertEntry

Result:
no goals
-- Mathlib/RingTheory/FractionalIdeal/Operations.lean
theorem mem_canonicalEquiv_apply {I : FractionalIdeal S P} {x : P'} :
    x ∈ canonicalEquiv S P P' I ↔
      ∃ y ∈ I,
        IsLocalization.map P' (RingHom.id R) (fun y (hy : y ∈ S) => show RingHom.id R y ∈ S from hy)
            (y : P) =
          x

Proof state:
R : Type u_1
inst✝⁶ : CommRing R
S : Submonoid R
P : Type u_2
inst✝⁵ : CommRing P
inst✝⁴ : Algebra R P
P' : Type u_3
inst✝³ : CommRing P'
inst✝² : Algebra R P'
inst✝¹ : IsLocalization S P
inst✝ : IsLocalization S P'
I : FractionalIdeal S P
x : P'
⊢ x ∈ (canonicalEquiv S P P') I ↔ ∃ y ∈ I, (IsLocalization.map P' (RingHom.id R) ⋯) y = x

Tactic:
rw [canonicalEquiv, mapEquiv_apply, mem_map]

Result:
R : Type u_1
inst✝⁶ : CommRing R
S : Submonoid R
P : Type u_2
inst✝⁵ : CommRing P
inst✝⁴ : Algebra R P
P' : Type u_3
inst✝³ : CommRing P'
inst✝² : Algebra R P'
inst✝¹ : IsLocalization S P
inst✝ : IsLocalization S P'
I : FractionalIdeal S P
x : P'
⊢ (∃ x_1 ∈ I,
      ↑(let __src := ringEquivOfRingEquiv P P' (RingEquiv.refl R) ⋯;
            { toEquiv := __src.toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ })
          x_1 =
        x) ↔
    ∃ y ∈ I, (IsLocalization.map P' (RingHom.id R) ⋯) y = x

Proof state:
R : Type u_1
inst✝⁶ : CommRing R
S : Submonoid R
P : Type u_2
inst✝⁵ : CommRing P
inst✝⁴ : Algebra R P
P' : Type u_3
inst✝³ : CommRing P'
inst✝² : Algebra R P'
inst✝¹ : IsLocalization S P
inst✝ : IsLocalization S P'
I : FractionalIdeal S P
x : P'
⊢ (∃ x_1 ∈ I,
      ↑(let __src := ringEquivOfRingEquiv P P' (RingEquiv.refl R) ⋯;
            { toEquiv := __src.toEquiv, map_mul' := ⋯, map_add' := ⋯, commutes' := ⋯ })
          x_1 =
        x) ↔
    ∃ y ∈ I, (IsLocalization.map P' (RingHom.id R) ⋯) y = x

Tactic:
exact ⟨fun ⟨y, mem, Eq⟩ => ⟨y, mem, Eq⟩, fun ⟨y, mem, Eq⟩ => ⟨y, mem, Eq⟩⟩

Result:
no goals
-- Mathlib/Algebra/Homology/ShortComplex/Homology.lean
@[reassoc (attr := simp)]
lemma homologyπ_comp_leftHomologyIso_inv :
    S.homologyπ ≫ S.leftHomologyIso.inv = S.leftHomologyπ

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
S : ShortComplex C
inst✝ : S.HasHomology
⊢ S.homologyπ ≫ S.leftHomologyIso.inv = S.leftHomologyπ

Tactic:
dsimp only [homologyπ]

Result:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
S : ShortComplex C
inst✝ : S.HasHomology
⊢ (S.leftHomologyπ ≫ S.leftHomologyIso.hom) ≫ S.leftHomologyIso.inv = S.leftHomologyπ

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
S : ShortComplex C
inst✝ : S.HasHomology
⊢ (S.leftHomologyπ ≫ S.leftHomologyIso.hom) ≫ S.leftHomologyIso.inv = S.leftHomologyπ

Tactic:
simp only [assoc, Iso.hom_inv_id, comp_id]

Result:
no goals
-- Mathlib/Data/Option/Basic.lean
theorem casesOn'_none_coe (f : Option α → β) (o : Option α) :
    casesOn' o (f none) (f ∘ (fun a ↦ ↑a)) = f o

Proof state:
α : Type u_1
β : Type u_2
f : Option α → β
o : Option α
⊢ o.casesOn' (f none) (f ∘ fun a => some a) = f o

Tactic:
cases o <;> rfl

Result:
no goals
-- Mathlib/Data/Set/Insert.lean
theorem diff_singleton_sSubset {s : Set α} {a : α} : s \ {a} ⊂ s ↔ a ∈ s :=
  sdiff_le.lt_iff_ne.trans <| sdiff_eq_left.not.trans <| by simp

Proof state:
α : Type u
s : Set α
a : α
⊢ ¬Disjoint s {a} ↔ a ∈ s

Tactic:
simp

Result:
no goals
-- Mathlib/Combinatorics/SetFamily/HarrisKleitman.lean
theorem IsLowerSet.card_inter_le_finset (h𝒜 : IsLowerSet (𝒜 : Set (Finset α)))
    (hℬ : IsUpperSet (ℬ : Set (Finset α))) :
    2 ^ Fintype.card α * #(𝒜 ∩ ℬ) ≤ #𝒜 * #ℬ

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
inst✝ : Fintype α
h𝒜 : IsLowerSet ↑𝒜
hℬ : IsUpperSet ↑ℬ
⊢ 2 ^ Fintype.card α * #(𝒜 ∩ ℬ) ≤ #𝒜 * #ℬ

Tactic:
rw [inter_comm, mul_comm #𝒜]

Result:
α : Type u_1
inst✝¹ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
inst✝ : Fintype α
h𝒜 : IsLowerSet ↑𝒜
hℬ : IsUpperSet ↑ℬ
⊢ 2 ^ Fintype.card α * #(ℬ ∩ 𝒜) ≤ #ℬ * #𝒜

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
𝒜 ℬ : Finset (Finset α)
inst✝ : Fintype α
h𝒜 : IsLowerSet ↑𝒜
hℬ : IsUpperSet ↑ℬ
⊢ 2 ^ Fintype.card α * #(ℬ ∩ 𝒜) ≤ #ℬ * #𝒜

Tactic:
exact hℬ.card_inter_le_finset h𝒜

Result:
no goals
-- Mathlib/Algebra/GroupWithZero/Defs.lean
lemma eq_zero_or_one_of_sq_eq_self (hx : x ^ 2 = x) : x = 0 ∨ x = 1 :=
  or_iff_not_imp_left.mpr (mul_left_injective₀ · <| by simpa [sq] using hx)

Proof state:
M₀ : Type u_1
inst✝ : CancelMonoidWithZero M₀
x : M₀
hx : x ^ 2 = x
x✝ : ¬x = 0
⊢ (fun a => a * x) x = (fun a => a * x) 1

Tactic:
simpa [sq] using hx

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/RawLemmas.lean
theorem get!_eq_get! [LawfulBEq α] [Inhabited β] (h : m.WF) {a : α} :
    get! m a = m.get! a

Proof state:
α : Type u
inst✝³ : BEq α
inst✝² : Hashable α
β : Type v
m : Raw α fun x => β
inst✝¹ : LawfulBEq α
inst✝ : Inhabited β
h : m.WF
a : α
⊢ get! m a = m.get! a

Tactic:
simp_to_raw using Raw₀.Const.get!_eq_get!

Result:
no goals
-- Mathlib/Data/ENNReal/Inv.lean
theorem inv_lt_one : a⁻¹ < 1 ↔ 1 < a

Proof state:
a : ℝ≥0∞
⊢ a⁻¹ < 1 ↔ 1 < a

Tactic:
rw [inv_lt_iff_inv_lt, inv_one]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Nat/Basic.lean
theorem max?_eq_some_iff' {xs : List Nat} :
    xs.max? = some a ↔ (a ∈ xs ∧ ∀ b ∈ xs, b ≤ a) :=
  max?_eq_some_iff
    (le_refl := Nat.le_refl)
    (max_eq_or := fun _ _ => Nat.max_def .. ▸ by split <;> simp)
    (max_le_iff := fun _ _ _ => Nat.max_le)

Proof state:
a : Nat
xs : List Nat
x✝¹ x✝ : Nat
⊢ (if x✝¹ ≤ x✝ then x✝ else x✝¹) = x✝¹ ∨ (if x✝¹ ≤ x✝ then x✝ else x✝¹) = x✝

Tactic:
split <;> simp

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Gamma/Basic.lean
theorem Gamma_zero : Gamma 0 = 0

Proof state:
⊢ Gamma 0 = 0

Tactic:
simpa only [← Complex.ofReal_zero, Complex.Gamma_ofReal, Complex.ofReal_inj] using
  Complex.Gamma_zero

Result:
no goals
-- Mathlib/Dynamics/Newton.lean
theorem newtonMap_apply_of_isUnit (h : IsUnit <| aeval x (derivative P)) :
    P.newtonMap x = x - h.unit⁻¹ * aeval x P

Proof state:
R : Type u_1
S : Type u_2
inst✝² : CommRing R
inst✝¹ : CommRing S
inst✝ : Algebra R S
P : R[X]
x : S
h : IsUnit ((aeval x) (derivative P))
⊢ P.newtonMap x = x - ↑h.unit⁻¹ * (aeval x) P

Tactic:
simp [newtonMap_apply, Ring.inverse, h]

Result:
no goals
-- Mathlib/Algebra/Homology/ShortComplex/Homology.lean
@[reassoc]
lemma leftRightHomologyComparison'_fac (h₁ : S.LeftHomologyData) (h₂ : S.RightHomologyData)
    [S.HasHomology] :
    leftRightHomologyComparison' h₁ h₂ = h₁.homologyIso.inv ≫ h₂.homologyIso.hom

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
S : ShortComplex C
h₁ : S.LeftHomologyData
h₂ : S.RightHomologyData
inst✝ : S.HasHomology
⊢ leftRightHomologyComparison' h₁ h₂ = h₁.homologyIso.inv ≫ h₂.homologyIso.hom

Tactic:
rw [leftRightHomologyComparison'_eq_leftHomologpMap'_comp_iso_hom_comp_rightHomologyMap'
  S.homologyData h₁ h₂]

Result:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
S : ShortComplex C
h₁ : S.LeftHomologyData
h₂ : S.RightHomologyData
inst✝ : S.HasHomology
⊢ leftHomologyMap' (𝟙 S) h₁ S.homologyData.left ≫
      S.homologyData.iso.hom ≫ rightHomologyMap' (𝟙 S) S.homologyData.right h₂ =
    h₁.homologyIso.inv ≫ h₂.homologyIso.hom

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
S : ShortComplex C
h₁ : S.LeftHomologyData
h₂ : S.RightHomologyData
inst✝ : S.HasHomology
⊢ leftHomologyMap' (𝟙 S) h₁ S.homologyData.left ≫
      S.homologyData.iso.hom ≫ rightHomologyMap' (𝟙 S) S.homologyData.right h₂ =
    h₁.homologyIso.inv ≫ h₂.homologyIso.hom

Tactic:
dsimp only [LeftHomologyData.homologyIso, LeftHomologyData.leftHomologyIso,
  Iso.symm, Iso.trans, Iso.refl, leftHomologyMapIso', leftHomologyIso,
  RightHomologyData.homologyIso, RightHomologyData.rightHomologyIso,
  rightHomologyMapIso', rightHomologyIso]

Result:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
S : ShortComplex C
h₁ : S.LeftHomologyData
h₂ : S.RightHomologyData
inst✝ : S.HasHomology
⊢ leftHomologyMap' (𝟙 S) h₁ S.homologyData.left ≫
      S.homologyData.iso.hom ≫ rightHomologyMap' (𝟙 S) S.homologyData.right h₂ =
    (leftHomologyMap' (𝟙 S) h₁ S.leftHomologyData ≫ leftHomologyMap' (𝟙 S) S.leftHomologyData S.homologyData.left) ≫
      (S.homologyData.iso.hom ≫ rightHomologyMap' (𝟙 S) S.homologyData.right S.rightHomologyData) ≫
        rightHomologyMap' (𝟙 S) S.rightHomologyData h₂

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroMorphisms C
S : ShortComplex C
h₁ : S.LeftHomologyData
h₂ : S.RightHomologyData
inst✝ : S.HasHomology
⊢ leftHomologyMap' (𝟙 S) h₁ S.homologyData.left ≫
      S.homologyData.iso.hom ≫ rightHomologyMap' (𝟙 S) S.homologyData.right h₂ =
    (leftHomologyMap' (𝟙 S) h₁ S.leftHomologyData ≫ leftHomologyMap' (𝟙 S) S.leftHomologyData S.homologyData.left) ≫
      (S.homologyData.iso.hom ≫ rightHomologyMap' (𝟙 S) S.homologyData.right S.rightHomologyData) ≫
        rightHomologyMap' (𝟙 S) S.rightHomologyData h₂

Tactic:
simp only [assoc, ← leftHomologyMap'_comp_assoc, id_comp, ← rightHomologyMap'_comp]

Result:
no goals
-- Mathlib/Algebra/Module/Submodule/Lattice.lean
theorem mem_iInf {ι} (p : ι → Submodule R M) {x} : (x ∈ ⨅ i, p i) ↔ ∀ i, x ∈ p i

Proof state:
R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Sort u_4
p : ι → Submodule R M
x : M
⊢ (∀ (i : ι), x ∈ ↑(p i)) ↔ ∀ (i : ι), x ∈ p i

Tactic:
rfl

Result:
no goals

Proof state:
R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Sort u_4
p : ι → Submodule R M
x : M
⊢ x ∈ ⨅ i, p i ↔ ∀ (i : ι), x ∈ p i

Tactic:
rw [← SetLike.mem_coe, iInf_coe, Set.mem_iInter]

Result:
R : Type u_1
M : Type u_3
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
ι : Sort u_4
p : ι → Submodule R M
x : M
⊢ (∀ (i : ι), x ∈ ↑(p i)) ↔ ∀ (i : ι), x ∈ p i