harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/Raw.lean
theorem containsThenInsert_fst_eq [BEq α] [Hashable α] {m : Raw α β} (h : m.WF) {a : α} {b : β a} :
    (m.containsThenInsert a b).1 = (Raw₀.containsThenInsert ⟨m, h.size_buckets_pos⟩ a b).1

Proof state:
α : Type u
β : α → Type v
inst✝¹ : BEq α
inst✝ : Hashable α
m : Raw α β
h : m.WF
a : α
b : β a
⊢ (m.containsThenInsert a b).fst = (Raw₀.containsThenInsert ⟨m, ⋯⟩ a b).fst

Tactic:
simp [Raw.containsThenInsert, h.size_buckets_pos]

Result:
no goals
-- Mathlib/Analysis/Normed/Group/Constructions.lean
/-- The seminorm of an element in a product space is `< r` if and only if the norm of each
component is. -/
@[to_additive pi_norm_lt_iff "The seminorm of an element in a product space is `< r` if and only
if the norm of each component is."]
lemma pi_norm_lt_iff' (hr : 0 < r) : ‖x‖ < r ↔ ∀ i, ‖x i‖ < r

Proof state:
ι : Type u_1
π : ι → Type u_4
inst✝¹ : Fintype ι
inst✝ : (i : ι) → SeminormedGroup (π i)
x : (i : ι) → π i
r : ℝ
hr : 0 < r
⊢ ‖x‖ < r ↔ ∀ (i : ι), ‖x i‖ < r

Tactic:
simp only [← dist_one_right, dist_pi_lt_iff hr, Pi.one_apply]

Result:
no goals
-- Mathlib/Order/BooleanAlgebra.lean
theorem sup_sdiff_inf (x y : α) : x \ y ⊔ x ⊓ y = x

Proof state:
α : Type u
inst✝ : GeneralizedBooleanAlgebra α
x y : α
⊢ x \ y ⊔ x ⊓ y = x

Tactic:
rw [sup_comm, sup_inf_sdiff]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/Transvection.lean
theorem det_transvection_of_ne (h : i ≠ j) (c : R) : det (transvection i j c) = 1

Proof state:
n : Type u_1
R : Type u₂
inst✝² : DecidableEq n
inst✝¹ : CommRing R
i j : n
inst✝ : Fintype n
h : i ≠ j
c : R
⊢ (transvection i j c).det = 1

Tactic:
rw [← updateRow_eq_transvection i j, det_updateRow_add_smul_self _ h, det_one]

Result:
no goals
-- Mathlib/Data/Rat/Defs.lean
protected lemma nonneg_antisymm : 0 ≤ q → 0 ≤ -q → q = 0

Proof state:
q : ℚ
⊢ 0 ≤ q.num → q.num ≤ 0 → q.num ≤ 0 ∧ 0 ≤ q.num

Tactic:
tauto

Result:
no goals

Proof state:
q : ℚ
⊢ 0 ≤ q → 0 ≤ -q → q = 0

Tactic:
simp_rw [← num_eq_zero, Int.le_antisymm_iff, ← num_nonneg, num_neg_eq_neg_num, Int.neg_nonneg]

Result:
q : ℚ
⊢ 0 ≤ q.num → q.num ≤ 0 → q.num ≤ 0 ∧ 0 ≤ q.num
-- Mathlib/Algebra/Group/Defs.lean
@[to_additive] lemma pow_mul_comm (a : M) (m n : ℕ) : a ^ m * a ^ n = a ^ n * a ^ m

Proof state:
M : Type u_2
inst✝ : Monoid M
a : M
m n : ℕ
⊢ a ^ m * a ^ n = a ^ n * a ^ m

Tactic:
rw [← pow_add, ← pow_add, Nat.add_comm]

Result:
no goals
-- Mathlib/LinearAlgebra/Span/Basic.lean
theorem map_subtype_span_singleton {p : Submodule R M} (x : p) :
    map p.subtype (R ∙ x) = R ∙ (x : M)

Proof state:
R : Type u_1
M : Type u_4
inst✝² : Semiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
p : Submodule R M
x : ↥p
⊢ map p.subtype (span R {x}) = span R {↑x}

Tactic:
simp [← span_image]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem Option.map_cast_apply {γ γ' : Type u} (h : γ = γ') (x : Option γ) :
    Option.map (cast h) x = cast (congrArg Option h) x

Proof state:
γ γ' : Type u
h : γ = γ'
x : Option γ
⊢ Option.map (cast h) x = cast ⋯ x

Tactic:
cases h

Result:
case refl
γ : Type u
x : Option γ
⊢ Option.map (cast ⋯) x = cast ⋯ x

Proof state:
case refl
γ : Type u
x : Option γ
⊢ Option.map (cast ⋯) x = cast ⋯ x

Tactic:
cases x <;> simp

Result:
no goals
-- Mathlib/CategoryTheory/Preadditive/Basic.lean
theorem neg_comp_neg : (-f) ≫ (-g) = f ≫ g

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
inst✝ : Preadditive C
P Q R : C
f : P ⟶ Q
g : Q ⟶ R
⊢ (-f) ≫ (-g) = f ≫ g

Tactic:
simp

Result:
no goals
-- Mathlib/RingTheory/Ideal/Cotangent.lean
lemma finrank_cotangentSpace_eq_zero_iff [IsNoetherianRing R] :
    finrank (ResidueField R) (CotangentSpace R) = 0 ↔ IsField R

Proof state:
R : Type u_1
inst✝² : CommRing R
inst✝¹ : IsLocalRing R
inst✝ : IsNoetherianRing R
⊢ finrank (ResidueField R) (CotangentSpace R) = 0 ↔ IsField R

Tactic:
rw [finrank_zero_iff, subsingleton_cotangentSpace_iff]

Result:
no goals
-- Mathlib/Algebra/SkewMonoidAlgebra/Basic.lean
theorem ofFinsupp_eq_zero {a} : (⟨a⟩ : SkewMonoidAlgebra k G) = 0 ↔ a = 0

Proof state:
k : Type u_1
G : Type u_2
inst✝ : AddCommMonoid k
a : G →₀ k
⊢ { toFinsupp := a } = 0 ↔ a = 0

Tactic:
rw [← ofFinsupp_zero, ofFinsupp_inj]

Result:
no goals
-- Mathlib/Algebra/Order/GroupWithZero/Unbundled.lean
@[gcongr, bound]
lemma pow_lt_pow_left₀ (hab : a < b)
    (ha : 0 ≤ a) : ∀ {n : ℕ}, n ≠ 0 → a ^ n < b ^ n
  | n + 1, _ => by
    simpa only [pow_succ] using mul_lt_mul_of_le_of_lt_of_nonneg_of_pos
      (pow_le_pow_left₀ ha hab.le _) hab ha (pow_pos (ha.trans_lt hab) _)

Proof state:
M₀ : Type u_1
inst✝⁴ : MonoidWithZero M₀
inst✝³ : PartialOrder M₀
a b : M₀
inst✝² : ZeroLEOneClass M₀
inst✝¹ : PosMulStrictMono M₀
inst✝ : MulPosStrictMono M₀
hab : a < b
ha : 0 ≤ a
n : ℕ
x✝ : n + 1 ≠ 0
⊢ a ^ (n + 1) < b ^ (n + 1)

Tactic:
simpa only [pow_succ] using mul_lt_mul_of_le_of_lt_of_nonneg_of_pos
  (pow_le_pow_left₀ ha hab.le _) hab ha (pow_pos (ha.trans_lt hab) _)

Result:
no goals
-- Mathlib/Topology/Inseparable.lean
theorem Topology.IsInducing.inseparable_iff (hf : IsInducing f) : (f x ~ᵢ f y) ↔ (x ~ᵢ y)

Proof state:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
x y : X
f : X → Y
hf : IsInducing f
⊢ (f x ~ᵢ f y) ↔ (x ~ᵢ y)

Tactic:
simp only [inseparable_iff_specializes_and, hf.specializes_iff]

Result:
no goals
-- Mathlib/Algebra/Homology/Embedding/TruncGE.lean
lemma restrictionToTruncGE'_f_eq_iso_hom_pOpcycles_iso_inv
    {i : ι} {i' : ι'} (hi' : e.f i = i') (hi : e.BoundaryGE i) :
    (K.restrictionToTruncGE' e).f i = (K.restrictionXIso e hi').hom ≫ K.pOpcycles i' ≫
      (K.truncGE'XIsoOpcycles e hi' hi).inv

Proof state:
ι : Type u_1
ι' : Type u_2
c : ComplexShape ι
c' : ComplexShape ι'
C : Type u_3
inst✝³ : Category.{u_4, u_3} C
inst✝² : HasZeroMorphisms C
K : HomologicalComplex C c'
e : c.Embedding c'
inst✝¹ : e.IsTruncGE
inst✝ : ∀ (i' : ι'), K.HasHomology i'
i : ι
i' : ι'
hi' : e.f i = i'
hi : e.BoundaryGE i
⊢ (K.restrictionToTruncGE' e).f i =
    (K.restrictionXIso e hi').hom ≫ K.pOpcycles i' ≫ (K.truncGE'XIsoOpcycles e hi' hi).inv

Tactic:
apply restrictionToTruncGE'.f_eq_iso_hom_pOpcycles_iso_inv

Result:
no goals
-- Mathlib/LinearAlgebra/FiniteDimensional/Defs.lean
theorem range_basisSingleton (ι : Type*) [Unique ι] (h : finrank K V = 1) (v : V) (hv : v ≠ 0) :
    Set.range (basisSingleton ι h v hv) = {v}

Proof state:
K : Type u
V : Type v
inst✝³ : DivisionRing K
inst✝² : AddCommGroup V
inst✝¹ : Module K V
ι : Type u_1
inst✝ : Unique ι
h : finrank K V = 1
v : V
hv : v ≠ 0
⊢ Set.range ⇑(basisSingleton ι h v hv) = {v}

Tactic:
rw [Set.range_unique, basisSingleton_apply]

Result:
no goals
-- Mathlib/RingTheory/Valuation/ValExtension.lean
theorem val_map_lt_one_iff (x : R) : vA (algebraMap R A x) < 1 ↔ vR x < 1

Proof state:
R : Type u_1
A : Type u_2
ΓR : Type u_3
ΓA : Type u_4
inst✝⁵ : CommRing R
inst✝⁴ : Ring A
inst✝³ : LinearOrderedCommMonoidWithZero ΓR
inst✝² : LinearOrderedCommMonoidWithZero ΓA
inst✝¹ : Algebra R A
vR : Valuation R ΓR
vA : Valuation A ΓA
inst✝ : IsValExtension vR vA
x : R
⊢ vA ((algebraMap R A) x) < 1 ↔ vR x < 1

Tactic:
simpa only [_root_.map_one, not_le] using (val_map_le_iff vR vA 1 x).not

Result:
no goals
-- Mathlib/Dynamics/BirkhoffSum/Average.lean
theorem birkhoffAverage_zero (f : α → α) (g : α → M) (x : α) :
    birkhoffAverage R f g 0 x = 0

Proof state:
R : Type u_1
α : Type u_2
M : Type u_3
inst✝² : DivisionSemiring R
inst✝¹ : AddCommMonoid M
inst✝ : Module R M
f : α → α
g : α → M
x : α
⊢ birkhoffAverage R f g 0 x = 0

Tactic:
simp [birkhoffAverage]

Result:
no goals
-- Mathlib/Order/UpperLower/Basic.lean
theorem compl_iSup (f : ι → UpperSet α) : (⨆ i, f i).compl = ⨆ i, (f i).compl :=
  LowerSet.ext <| by simp only [coe_compl, coe_iSup, compl_iInter, LowerSet.coe_iSup]

Proof state:
α : Type u_1
ι : Sort u_4
inst✝ : LE α
f : ι → UpperSet α
⊢ ↑(⨆ i, f i).compl = ↑(⨆ i, (f i).compl)

Tactic:
simp only [coe_compl, coe_iSup, compl_iInter, LowerSet.coe_iSup]

Result:
no goals
-- Mathlib/RingTheory/HahnSeries/Addition.lean
@[simp]
protected lemma map_add [AddMonoid S] (f : R →+ S) {x y : HahnSeries Γ R} :
    ((x + y).map f : HahnSeries Γ S) = x.map f + y.map f

Proof state:
Γ : Type u_1
R : Type u_3
S : Type u_4
inst✝² : PartialOrder Γ
inst✝¹ : AddMonoid R
inst✝ : AddMonoid S
f : R →+ S
x y : HahnSeries Γ R
⊢ (x + y).map f = x.map f + y.map f

Tactic:
ext

Result:
case coeff.h
Γ : Type u_1
R : Type u_3
S : Type u_4
inst✝² : PartialOrder Γ
inst✝¹ : AddMonoid R
inst✝ : AddMonoid S
f : R →+ S
x y : HahnSeries Γ R
x✝ : Γ
⊢ ((x + y).map f).coeff x✝ = (x.map f + y.map f).coeff x✝

Proof state:
case coeff.h
Γ : Type u_1
R : Type u_3
S : Type u_4
inst✝² : PartialOrder Γ
inst✝¹ : AddMonoid R
inst✝ : AddMonoid S
f : R →+ S
x y : HahnSeries Γ R
x✝ : Γ
⊢ ((x + y).map f).coeff x✝ = (x.map f + y.map f).coeff x✝

Tactic:
simp

Result:
no goals
-- Mathlib/Probability/Kernel/Basic.lean
lemma const_add (β : Type*) [MeasurableSpace β] (μ ν : Measure α) :
    const β (μ + ν) = const β μ + const β ν

Proof state:
case h.h
α : Type u_1
mα : MeasurableSpace α
β : Type u_4
inst✝ : MeasurableSpace β
μ ν : Measure α
a✝¹ : β
s✝ : Set α
a✝ : MeasurableSet s✝
⊢ ((const β (μ + ν)) a✝¹) s✝ = ((const β μ + const β ν) a✝¹) s✝

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
mα : MeasurableSpace α
β : Type u_4
inst✝ : MeasurableSpace β
μ ν : Measure α
⊢ const β (μ + ν) = const β μ + const β ν

Tactic:
ext

Result:
case h.h
α : Type u_1
mα : MeasurableSpace α
β : Type u_4
inst✝ : MeasurableSpace β
μ ν : Measure α
a✝¹ : β
s✝ : Set α
a✝ : MeasurableSet s✝
⊢ ((const β (μ + ν)) a✝¹) s✝ = ((const β μ + const β ν) a✝¹) s✝
-- Mathlib/Topology/Sober.lean
theorem IsIrreducible.isGenericPoint_genericPoint [QuasiSober α] {S : Set α}
    (hS : IsIrreducible S) (hS' : IsClosed S) :
    IsGenericPoint hS.genericPoint S

Proof state:
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : QuasiSober α
S : Set α
hS : IsIrreducible S
hS' : IsClosed S
⊢ IsGenericPoint hS.genericPoint S

Tactic:
convert hS.isGenericPoint_genericPoint_closure

Result:
case h.e'_4
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : QuasiSober α
S : Set α
hS : IsIrreducible S
hS' : IsClosed S
⊢ S = closure S

Proof state:
case h.e'_4
α : Type u_1
inst✝¹ : TopologicalSpace α
inst✝ : QuasiSober α
S : Set α
hS : IsIrreducible S
hS' : IsClosed S
⊢ S = closure S

Tactic:
exact hS'.closure_eq.symm

Result:
no goals
-- Mathlib/Algebra/Group/Submonoid/Basic.lean
theorem coe_iInf {ι : Sort*} {S : ι → Submonoid M} : (↑(⨅ i, S i) : Set M) = ⋂ i, S i

Proof state:
M : Type u_1
inst✝ : MulOneClass M
ι : Sort u_4
S : ι → Submonoid M
⊢ ↑(⨅ i, S i) = ⋂ i, ↑(S i)

Tactic:
simp only [iInf, coe_sInf, Set.biInter_range]

Result:
no goals
-- Mathlib/CategoryTheory/SmallObject/Iteration/Basic.lean
lemma arrow_mk_mapObj {j₁ j₂ : J} (iter₁ : Φ.Iteration j₁) (iter₂ : Φ.Iteration j₂)
    {k₁ k₂ : J} (h₁₂ : k₁ ≤ k₂) (h₁ : k₁ ≤ j₁) (h₂ : k₂ ≤ j₂) (hj : j₁ ≤ j₂) :
    Arrow.mk (mapObj iter₁ iter₂ h₁₂ h₁ h₂ hj) =
      arrowMap iter₂.F k₁ k₂ h₁₂ h₂

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₂ : J
iter₁ : Φ.Iteration j₁
iter₂ : Φ.Iteration j₂
k₁ k₂ : J
h₁₂ : k₁ ≤ k₂
h₁ : k₁ ≤ j₁
h₂ : k₂ ≤ j₂
hj : j₁ ≤ j₂
⊢ Arrow.mk (iter₁.mapObj iter₂ h₁₂ h₁ h₂ hj) = arrowMap iter₂.F k₁ k₂ h₁₂ h₂

Tactic:
simp [mapObj, arrowMap]

Result:
no goals
-- Mathlib/Tactic/NormNum/Result.lean
theorem IsRat.to_raw_eq {n : ℤ} {d : ℕ} [DivisionRing α] :
    ∀ {a}, IsRat (a : α) n d → a = Rat.rawCast n d
  | _, ⟨inv, rfl⟩ => by simp [div_eq_mul_inv]

Proof state:
α : Type u
n : ℤ
d : ℕ
inst✝ : DivisionRing α
inv : Invertible ↑d
⊢ ↑n * ⅟↑d = Rat.rawCast n d

Tactic:
simp [div_eq_mul_inv]

Result:
no goals
-- Mathlib/Data/Nat/Find.lean
@[simp]
lemma findGreatest_of_not (h : ¬ P (n + 1)) : findGreatest P (n + 1) = findGreatest P n

Proof state:
P : ℕ → Prop
inst✝ : DecidablePred P
n : ℕ
h : ¬P (n + 1)
⊢ findGreatest P (n + 1) = findGreatest P n

Tactic:
simp [Nat.findGreatest, h]

Result:
no goals
-- Mathlib/Topology/Algebra/Group/Basic.lean
theorem inv_mem_connectedComponent_one {G : Type*} [TopologicalSpace G] [Group G]
    [IsTopologicalGroup G] {g : G} (hg : g ∈ connectedComponent (1 : G)) :
    g⁻¹ ∈ connectedComponent (1 : G)

Proof state:
G : Type u_1
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
g : G
hg : g ∈ connectedComponent 1
⊢ g⁻¹ ∈ connectedComponent 1⁻¹

Tactic:
exact
  Continuous.image_connectedComponent_subset continuous_inv _
    ((Set.mem_image _ _ _).mp ⟨g, hg, rfl⟩)

Result:
no goals

Proof state:
G : Type u_1
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
g : G
hg : g ∈ connectedComponent 1
⊢ g⁻¹ ∈ connectedComponent 1

Tactic:
rw [← inv_one]

Result:
G : Type u_1
inst✝² : TopologicalSpace G
inst✝¹ : Group G
inst✝ : IsTopologicalGroup G
g : G
hg : g ∈ connectedComponent 1
⊢ g⁻¹ ∈ connectedComponent 1⁻¹
-- Mathlib/Algebra/Algebra/Operations.lean
theorem map_unop_mul (M N : Submodule R Aᵐᵒᵖ) :
    map (↑(opLinearEquiv R : A ≃ₗ[R] Aᵐᵒᵖ).symm : Aᵐᵒᵖ →ₗ[R] A) (M * N) =
      map (↑(opLinearEquiv R : A ≃ₗ[R] Aᵐᵒᵖ).symm : Aᵐᵒᵖ →ₗ[R] A) N *
        map (↑(opLinearEquiv R : A ≃ₗ[R] Aᵐᵒᵖ).symm : Aᵐᵒᵖ →ₗ[R] A) M :=
  have : Function.Injective (↑(opLinearEquiv R : A ≃ₗ[R] Aᵐᵒᵖ) : A →ₗ[R] Aᵐᵒᵖ) :=
    LinearEquiv.injective _
  map_injective_of_injective this <| by
    rw [← map_comp, map_op_mul, ← map_comp, ← map_comp, LinearEquiv.comp_coe,
      LinearEquiv.symm_trans_self, LinearEquiv.refl_toLinearMap, map_id, map_id, map_id]

Proof state:
R : Type u
inst✝² : CommSemiring R
A : Type v
inst✝¹ : Semiring A
inst✝ : Algebra R A
M N : Submodule R Aᵐᵒᵖ
this : Function.Injective ⇑↑(opLinearEquiv R)
⊢ map (↑(opLinearEquiv R)) (map (↑(opLinearEquiv R).symm) (M * N)) =
    map (↑(opLinearEquiv R)) (map (↑(opLinearEquiv R).symm) N * map (↑(opLinearEquiv R).symm) M)

Tactic:
rw [← map_comp, map_op_mul, ← map_comp, ← map_comp, LinearEquiv.comp_coe,
  LinearEquiv.symm_trans_self, LinearEquiv.refl_toLinearMap, map_id, map_id, map_id]

Result:
no goals
-- Mathlib/Algebra/Ring/NonZeroDivisors.lean
lemma mul_cancel_right_mem_nonZeroDivisors (hr : r ∈ R⁰) : x * r = y * r ↔ x = y

Proof state:
R : Type u_1
inst✝ : Ring R
x y r : R
hr : r ∈ R⁰
h : x * r = y * r
⊢ x = y

Tactic:
rw [← sub_eq_zero, ← mul_right_mem_nonZeroDivisors_eq_zero_iff hr, sub_mul, h, sub_self]

Result:
no goals
-- Mathlib/CategoryTheory/Localization/CalculusOfFractions.lean
lemma LeftFractionRel.op {X Y : C} {z₁ z₂ : W.LeftFraction X Y}
    (h : LeftFractionRel z₁ z₂) : RightFractionRel z₁.op z₂.op

Proof state:
C : Type u_1
inst✝ : Category.{u_3, u_1} C
W : MorphismProperty C
X Y : C
z₁ z₂ : W.LeftFraction X Y
h : LeftFractionRel z₁ z₂
⊢ RightFractionRel z₁.op z₂.op

Tactic:
obtain ⟨Z, t₁, t₂, hs, hf, ht⟩ := h

Result:
case intro.intro.intro.intro.intro
C : Type u_1
inst✝ : Category.{u_3, u_1} C
W : MorphismProperty C
X Y : C
z₁ z₂ : W.LeftFraction X Y
Z : C
t₁ : z₁.Y' ⟶ Z
t₂ : z₂.Y' ⟶ Z
hs : z₁.s ≫ t₁ = z₂.s ≫ t₂
hf : z₁.f ≫ t₁ = z₂.f ≫ t₂
ht : W (z₁.s ≫ t₁)
⊢ RightFractionRel z₁.op z₂.op

Proof state:
case intro.intro.intro.intro.intro
C : Type u_1
inst✝ : Category.{u_3, u_1} C
W : MorphismProperty C
X Y : C
z₁ z₂ : W.LeftFraction X Y
Z : C
t₁ : z₁.Y' ⟶ Z
t₂ : z₂.Y' ⟶ Z
hs : z₁.s ≫ t₁ = z₂.s ≫ t₂
hf : z₁.f ≫ t₁ = z₂.f ≫ t₂
ht : W (z₁.s ≫ t₁)
⊢ RightFractionRel z₁.op z₂.op

Tactic:
exact ⟨Opposite.op Z, t₁.op, t₂.op, Quiver.Hom.unop_inj hs,
  Quiver.Hom.unop_inj hf, ht⟩

Result:
no goals
-- Mathlib/MeasureTheory/Constructions/Projective.lean
lemma measure_univ_eq (hμ : IsProjectiveLimit μ P) (I : Finset ι) :
    μ univ = P I univ

Proof state:
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → MeasurableSpace (α i)
P : (J : Finset ι) → Measure ((j : { x // x ∈ J }) → α ↑j)
μ : Measure ((i : ι) → α i)
hμ : IsProjectiveLimit μ P
I : Finset ι
⊢ μ univ = (P I) univ

Tactic:
rw [← cylinder_univ I, hμ.measure_cylinder _ MeasurableSet.univ]

Result:
no goals
-- Mathlib/Analysis/Analytic/Basic.lean
theorem ContinuousLinearMap.comp_hasFPowerSeriesWithinOnBall (g : F →L[𝕜] G)
    (h : HasFPowerSeriesWithinOnBall f p s x r) :
    HasFPowerSeriesWithinOnBall (g ∘ f) (g.compFormalMultilinearSeries p) s x r where
  r_le := h.r_le.trans (p.radius_le_radius_continuousLinearMap_comp _)
  r_pos := h.r_pos
  hasSum hy h'y

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
G : Type u_4
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : NormedAddCommGroup E
inst✝⁴ : NormedSpace 𝕜 E
inst✝³ : NormedAddCommGroup F
inst✝² : NormedSpace 𝕜 F
inst✝¹ : NormedAddCommGroup G
inst✝ : NormedSpace 𝕜 G
f : E → F
p : FormalMultilinearSeries 𝕜 E F
s : Set E
x : E
r : ℝ≥0∞
g : F →L[𝕜] G
h : HasFPowerSeriesWithinOnBall f p s x r
y✝ : E
hy : x + y✝ ∈ insert x s
h'y : y✝ ∈ EMetric.ball 0 r
⊢ HasSum (fun n => (g.compFormalMultilinearSeries p n) fun x => y✝) ((⇑g ∘ f) (x + y✝))

Tactic:
simpa only [ContinuousLinearMap.compFormalMultilinearSeries_apply,
  ContinuousLinearMap.compContinuousMultilinearMap_coe, Function.comp_apply] using
  g.hasSum (h.hasSum hy h'y)

Result:
no goals
-- Mathlib/Combinatorics/Young/YoungDiagram.lean
theorem exists_not_mem_col (μ : YoungDiagram) (j : ℕ) : ∃ i, (i, j) ∉ μ.cells

Proof state:
μ : YoungDiagram
j : ℕ
⊢ ∃ i, (i, j) ∉ μ.cells

Tactic:
convert μ.transpose.exists_not_mem_row j using 1

Result:
case h.e'_2
μ : YoungDiagram
j : ℕ
⊢ (fun i => (i, j) ∉ μ.cells) = fun j_1 => (j, j_1) ∉ μ.transpose

Proof state:
case h.e'_2
μ : YoungDiagram
j : ℕ
⊢ (fun i => (i, j) ∉ μ.cells) = fun j_1 => (j, j_1) ∉ μ.transpose

Tactic:
simp

Result:
no goals
-- Mathlib/Tactic/NormNum/Prime.lean
theorem minFacHelper_2 {n k k' : ℕ} (e : k + 2 = k') (nk : ¬ Nat.Prime k)
    (h : MinFacHelper n k) : MinFacHelper n k'

Proof state:
n k k' : ℕ
e : k + 2 = k'
nk : ¬Nat.Prime n.minFac
h : MinFacHelper n k
h2 : n.minFac = k
⊢ False

Tactic:
exact nk <| minFac_prime h.one_lt.ne'

Result:
no goals

Proof state:
n k k' : ℕ
e : k + 2 = k'
nk : ¬Nat.Prime k
h : MinFacHelper n k
h2 : n.minFac = k
⊢ False

Tactic:
rw [← h2] at nk

Result:
n k k' : ℕ
e : k + 2 = k'
nk : ¬Nat.Prime n.minFac
h : MinFacHelper n k
h2 : n.minFac = k
⊢ False

Proof state:
n k k' : ℕ
e : k + 2 = k'
nk : ¬Nat.Prime k
h : MinFacHelper n k
⊢ MinFacHelper n k'

Tactic:
refine minFacHelper_1 e h fun h2 ↦ ?_

Result:
n k k' : ℕ
e : k + 2 = k'
nk : ¬Nat.Prime k
h : MinFacHelper n k
h2 : n.minFac = k
⊢ False
-- Mathlib/Analysis/SpecialFunctions/Log/NegMulLog.lean
@[simp] lemma negMulLog_zero : negMulLog (0 : ℝ) = 0

Proof state:
⊢ negMulLog 0 = 0

Tactic:
simp [negMulLog]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Trigonometric/Inverse.lean
theorem sin_arcsin' {x : ℝ} (hx : x ∈ Icc (-1 : ℝ) 1) : sin (arcsin x) = x

Proof state:
x : ℝ
hx : x ∈ Icc (-1) 1
⊢ sin (arcsin x) = x

Tactic:
simpa [arcsin, IccExtend_of_mem _ _ hx, -OrderIso.apply_symm_apply] using
  Subtype.ext_iff.1 (sinOrderIso.apply_symm_apply ⟨x, hx⟩)

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/BilinearForm.lean
theorem Matrix.toBilin_basisFun : Matrix.toBilin (Pi.basisFun R₁ n) = Matrix.toBilin'

Proof state:
case h.h.h.h.h
R₁ : Type u_1
inst✝² : CommSemiring R₁
n : Type u_5
inst✝¹ : Fintype n
inst✝ : DecidableEq n
M : Matrix n n R₁
i✝¹ i✝ : n
⊢ (((toBilin (Pi.basisFun R₁ n)) M ∘ₗ single R₁ (fun i => R₁) i✝¹) 1 ∘ₗ single R₁ (fun i => R₁) i✝) 1 =
    ((toBilin' M ∘ₗ single R₁ (fun i => R₁) i✝¹) 1 ∘ₗ single R₁ (fun i => R₁) i✝) 1

Tactic:
simp only [coe_comp, coe_single, Function.comp_apply, toBilin_apply, Pi.basisFun_repr,
  toBilin'_apply]

Result:
no goals

Proof state:
R₁ : Type u_1
inst✝² : CommSemiring R₁
n : Type u_5
inst✝¹ : Fintype n
inst✝ : DecidableEq n
⊢ toBilin (Pi.basisFun R₁ n) = toBilin'

Tactic:
ext M

Result:
case h.h.h.h.h
R₁ : Type u_1
inst✝² : CommSemiring R₁
n : Type u_5
inst✝¹ : Fintype n
inst✝ : DecidableEq n
M : Matrix n n R₁
i✝¹ i✝ : n
⊢ (((toBilin (Pi.basisFun R₁ n)) M ∘ₗ single R₁ (fun i => R₁) i✝¹) 1 ∘ₗ single R₁ (fun i => R₁) i✝) 1 =
    ((toBilin' M ∘ₗ single R₁ (fun i => R₁) i✝¹) 1 ∘ₗ single R₁ (fun i => R₁) i✝) 1
-- Mathlib/CategoryTheory/Limits/Shapes/ZeroMorphisms.lean
theorem zeroIsoIsTerminal_inv {X : C} (t : IsTerminal X) : (zeroIsoIsTerminal t).inv = 0

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasZeroObject C
inst✝ : HasZeroMorphisms C
X : C
t : IsTerminal X
⊢ (zeroIsoIsTerminal t).inv = 0

Tactic:
ext

Result:
no goals
-- Mathlib/Topology/Algebra/InfiniteSum/NatInt.lean
/-- "iff" version of `Multipliable.of_nat_of_neg_add_one`. -/
@[to_additive "\"iff\" version of `Summable.of_nat_of_neg_add_one`."]
lemma multipliable_int_iff_multipliable_nat_and_neg_add_one {f : ℤ → G} : Multipliable f ↔
    (Multipliable fun n : ℕ ↦ f n) ∧ (Multipliable fun n : ℕ ↦ f (-(n + 1)))

Proof state:
case refine_1
G : Type u_2
inst✝³ : CommGroup G
inst✝² : UniformSpace G
inst✝¹ : UniformGroup G
inst✝ : CompleteSpace G
f : ℤ → G
p : Multipliable f
⊢ Injective Nat.cast

case refine_2
G : Type u_2
inst✝³ : CommGroup G
inst✝² : UniformSpace G
inst✝¹ : UniformGroup G
inst✝ : CompleteSpace G
f : ℤ → G
p : Multipliable f
⊢ Injective fun n => -(↑n + 1)

Tactic:
exacts [Nat.cast_injective, @Int.negSucc.inj]

Result:
no goals

Proof state:
G : Type u_2
inst✝³ : CommGroup G
inst✝² : UniformSpace G
inst✝¹ : UniformGroup G
inst✝ : CompleteSpace G
f : ℤ → G
⊢ Multipliable f ↔ (Multipliable fun n => f ↑n) ∧ Multipliable fun n => f (-(↑n + 1))

Tactic:
refine ⟨fun p ↦ ⟨?_, ?_⟩, fun ⟨hf₁, hf₂⟩ ↦ Multipliable.of_nat_of_neg_add_one hf₁ hf₂⟩ <;>
apply p.comp_injective

Result:
case refine_1
G : Type u_2
inst✝³ : CommGroup G
inst✝² : UniformSpace G
inst✝¹ : UniformGroup G
inst✝ : CompleteSpace G
f : ℤ → G
p : Multipliable f
⊢ Injective Nat.cast

case refine_2
G : Type u_2
inst✝³ : CommGroup G
inst✝² : UniformSpace G
inst✝¹ : UniformGroup G
inst✝ : CompleteSpace G
f : ℤ → G
p : Multipliable f
⊢ Injective fun n => -(↑n + 1)
-- Mathlib/RingTheory/Ideal/Operations.lean
theorem sup_multiset_prod_eq_top {s : Multiset (Ideal R)} (h : ∀  p ∈ s, I ⊔ p = ⊤) :
    I ⊔ Multiset.prod s = ⊤ :=
  Multiset.prod_induction (I ⊔ · = ⊤) s (fun _ _ hp hq ↦ (sup_mul_eq_of_coprime_left hp).trans hq)
    (by simp only [one_eq_top, ge_iff_le, top_le_iff, le_top, sup_of_le_right]) h

Proof state:
R : Type u
inst✝ : CommSemiring R
I : Ideal R
s : Multiset (Ideal R)
h : ∀ p ∈ s, I ⊔ p = ⊤
⊢ (fun x => I ⊔ x = ⊤) 1

Tactic:
simp only [one_eq_top, ge_iff_le, top_le_iff, le_top, sup_of_le_right]

Result:
no goals
-- Mathlib/RingTheory/TwoSidedIdeal/Operations.lean
@[simp]
lemma mem_asIdeal {I : TwoSidedIdeal R} {x : R} :
    x ∈ asIdeal I ↔ x ∈ I

Proof state:
R : Type u_1
inst✝ : Ring R
I : TwoSidedIdeal R
x : R
⊢ x ∈ asIdeal I ↔ x ∈ I

Tactic:
simp [asIdeal]

Result:
no goals
-- Mathlib/RepresentationTheory/Basic.lean
theorem asAlgebraHom_of (g : G) : asAlgebraHom ρ (of k G g) = ρ g

Proof state:
k : Type u_1
G : Type u_2
V : Type u_3
inst✝³ : CommSemiring k
inst✝² : Monoid G
inst✝¹ : AddCommMonoid V
inst✝ : Module k V
ρ : Representation k G V
g : G
⊢ ρ.asAlgebraHom ((of k G) g) = ρ g

Tactic:
simp only [MonoidAlgebra.of_apply, asAlgebraHom_single, one_smul]

Result:
no goals
-- Mathlib/Algebra/Order/Group/Pointwise/Interval.lean
theorem preimage_mul_const_Ioc (a b : α) {c : α} (h : 0 < c) :
    (fun x => x * c) ⁻¹' Ioc a b = Ioc (a / c) (b / c)

Proof state:
α : Type u_1
inst✝ : LinearOrderedField α
a b c : α
h : 0 < c
⊢ (fun x => x * c) ⁻¹' Ioc a b = Ioc (a / c) (b / c)

Tactic:
simp [← Ioi_inter_Iic, h]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem filter_reverse (p : α → Bool) (l : Array α) : (l.reverse.filter p) = (l.filter p).reverse

Proof state:
α : Type u_1
p : α → Bool
l : Array α
⊢ filter p l.reverse = (filter p l).reverse

Tactic:
cases l

Result:
case mk
α : Type u_1
p : α → Bool
toList✝ : List α
⊢ filter p { toList := toList✝ }.reverse = (filter p { toList := toList✝ }).reverse

Proof state:
case mk
α : Type u_1
p : α → Bool
toList✝ : List α
⊢ filter p { toList := toList✝ }.reverse = (filter p { toList := toList✝ }).reverse

Tactic:
simp

Result:
no goals