harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/RingTheory/FractionalIdeal/Operations.lean
theorem canonicalEquiv_canonicalEquiv (P'' : Type*) [CommRing P''] [Algebra R P'']
    [IsLocalization S P''] (I : FractionalIdeal S P) :
    canonicalEquiv S P' P'' (canonicalEquiv S P P' I) = canonicalEquiv S P P'' I

Proof state:
case a
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'
P'' : Type u_5
inst✝² : CommRing P''
inst✝¹ : Algebra R P''
inst✝ : IsLocalization S P''
I : FractionalIdeal S P
x✝ : P''
⊢ x✝ ∈ (canonicalEquiv S P' P'') ((canonicalEquiv S P P') I) ↔ x✝ ∈ (canonicalEquiv S P P'') I

Tactic:
simp only [IsLocalization.map_map, RingHomInvPair.comp_eq₂, mem_canonicalEquiv_apply,
  exists_prop, exists_exists_and_eq_and]

Result:
no goals

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'
P'' : Type u_5
inst✝² : CommRing P''
inst✝¹ : Algebra R P''
inst✝ : IsLocalization S P''
I : FractionalIdeal S P
⊢ (canonicalEquiv S P' P'') ((canonicalEquiv S P P') I) = (canonicalEquiv S P P'') I

Tactic:
ext

Result:
case a
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'
P'' : Type u_5
inst✝² : CommRing P''
inst✝¹ : Algebra R P''
inst✝ : IsLocalization S P''
I : FractionalIdeal S P
x✝ : P''
⊢ x✝ ∈ (canonicalEquiv S P' P'') ((canonicalEquiv S P P') I) ↔ x✝ ∈ (canonicalEquiv S P P'') I
-- Mathlib/Order/Interval/Set/SuccPred.lean
lemma Iic_pred_eq_Iio_of_not_isMin (hb : ¬ IsMin b) : Iic (pred b) = Iio b

Proof state:
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : PredOrder α
b : α
hb : ¬IsMin b
⊢ Iic (pred b) = Iio b

Tactic:
ext x

Result:
case h
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : PredOrder α
b : α
hb : ¬IsMin b
x : α
⊢ x ∈ Iic (pred b) ↔ x ∈ Iio b

Proof state:
case h
α : Type u_1
inst✝¹ : LinearOrder α
inst✝ : PredOrder α
b : α
hb : ¬IsMin b
x : α
⊢ x ∈ Iic (pred b) ↔ x ∈ Iio b

Tactic:
rw [mem_Iic, mem_Iio, le_pred_iff_of_not_isMin hb]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/RBMap/WF.lean
theorem Ordered.setRed {t : RBNode α} : (setRed t).Ordered cmp ↔ t.Ordered cmp

Proof state:
α : Type u_1
cmp : α → α → Ordering
t : RBNode α
⊢ Ordered cmp t.setRed ↔ Ordered cmp t

Tactic:
unfold setRed

Result:
α : Type u_1
cmp : α → α → Ordering
t : RBNode α
⊢ Ordered cmp
      (match t with
      | node c a v b => node red a v b
      | nil => nil) ↔
    Ordered cmp t

Proof state:
α : Type u_1
cmp : α → α → Ordering
t : RBNode α
⊢ Ordered cmp
      (match t with
      | node c a v b => node red a v b
      | nil => nil) ↔
    Ordered cmp t

Tactic:
split <;> simp [Ordered]

Result:
no goals
-- Mathlib/Analysis/Complex/UpperHalfPlane/Metric.lean
theorem cosh_dist (z w : ℍ) : cosh (dist z w) = 1 + dist (z : ℂ) w ^ 2 / (2 * z.im * w.im)

Proof state:
z w : ℍ
⊢ cosh (dist z w) = 1 + dist ↑z ↑w ^ 2 / (2 * z.im * w.im)

Tactic:
rw [dist_eq, cosh_two_mul, cosh_sq', add_assoc, ← two_mul, sinh_arsinh, div_pow, mul_pow,
  sq_sqrt, sq (2 : ℝ), mul_assoc, ← mul_div_assoc, mul_assoc, mul_div_mul_left] <;> positivity

Result:
no goals
-- Mathlib/Tactic/NormNum/Eq.lean
theorem isRat_eq_false [Ring α] [CharZero α] : {a b : α} → {na nb : ℤ} → {da db : ℕ} →
    IsRat a na da → IsRat b nb db →
    decide (Int.mul na (.ofNat db) = Int.mul nb (.ofNat da)) = false → ¬a = b
  | _, _, _, _, _, _, ⟨_, rfl⟩, ⟨_, rfl⟩, h => by
    rw [Rat.invOf_denom_swap]; exact mod_cast of_decide_eq_false h

Proof state:
α : Type u_1
inst✝¹ : Ring α
inst✝ : CharZero α
num✝¹ num✝ : ℤ
denom✝¹ denom✝ : ℕ
inv✝¹ : Invertible ↑denom✝¹
inv✝ : Invertible ↑denom✝
h : decide (num✝¹.mul (Int.ofNat denom✝) = num✝.mul (Int.ofNat denom✝¹)) = false
⊢ ¬↑num✝¹ * ↑denom✝ = ↑num✝ * ↑denom✝¹

Tactic:
exact mod_cast of_decide_eq_false h

Result:
no goals

Proof state:
α : Type u_1
inst✝¹ : Ring α
inst✝ : CharZero α
num✝¹ num✝ : ℤ
denom✝¹ denom✝ : ℕ
inv✝¹ : Invertible ↑denom✝¹
inv✝ : Invertible ↑denom✝
h : decide (num✝¹.mul (Int.ofNat denom✝) = num✝.mul (Int.ofNat denom✝¹)) = false
⊢ ¬↑num✝¹ * ⅟↑denom✝¹ = ↑num✝ * ⅟↑denom✝

Tactic:
rw [Rat.invOf_denom_swap]

Result:
α : Type u_1
inst✝¹ : Ring α
inst✝ : CharZero α
num✝¹ num✝ : ℤ
denom✝¹ denom✝ : ℕ
inv✝¹ : Invertible ↑denom✝¹
inv✝ : Invertible ↑denom✝
h : decide (num✝¹.mul (Int.ofNat denom✝) = num✝.mul (Int.ofNat denom✝¹)) = false
⊢ ¬↑num✝¹ * ↑denom✝ = ↑num✝ * ↑denom✝¹
-- Mathlib/Data/Finset/Defs.lean
@[simp] lemma forall_mem_not_eq' {s : Finset α} {a : α} : (∀ b ∈ s, ¬ b = a) ↔ a ∉ s

Proof state:
α : Type u_1
s : Finset α
a : α
⊢ (∀ b ∈ s, ¬b = a) ↔ a ∉ s

Tactic:
aesop

Result:
no goals
-- Mathlib/Probability/Kernel/RadonNikodym.lean
lemma rnDeriv_eq_top_iff (κ η : Kernel α γ) (a : α) (x : γ) :
    rnDeriv κ η a x = ∞ ↔ (a, x) ∈ mutuallySingularSet κ η

Proof state:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
a : α
x : γ
⊢ κ.rnDeriv η a x = ⊤ ↔ (a, x) ∈ κ.mutuallySingularSet η

Tactic:
simp only [rnDeriv, ENNReal.div_eq_top, ne_eq, ENNReal.ofReal_eq_zero, not_le,
  tsub_le_iff_right, zero_add, ENNReal.ofReal_ne_top, not_false_eq_true, and_true, or_false,
  mutuallySingularSet, mem_setOf_eq, and_iff_right_iff_imp]

Result:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
a : α
x : γ
⊢ 1 ≤ κ.rnDerivAux (κ + η) a x → 0 < κ.rnDerivAux (κ + η) a x

Proof state:
α : Type u_1
γ : Type u_2
mα : MeasurableSpace α
mγ : MeasurableSpace γ
hαγ : MeasurableSpace.CountableOrCountablyGenerated α γ
κ η : Kernel α γ
a : α
x : γ
⊢ 1 ≤ κ.rnDerivAux (κ + η) a x → 0 < κ.rnDerivAux (κ + η) a x

Tactic:
exact fun h ↦ zero_lt_one.trans_le h

Result:
no goals
-- Mathlib/Analysis/NormedSpace/Pointwise.lean
theorem closedBall_sub_ball (hε : 0 ≤ ε) (hδ : 0 < δ) (a b : E) :
    closedBall a ε - ball b δ = ball (a - b) (ε + δ)

Proof state:
E : Type u_2
inst✝¹ : SeminormedAddCommGroup E
inst✝ : NormedSpace ℝ E
δ ε : ℝ
hε : 0 ≤ ε
hδ : 0 < δ
a b : E
⊢ Metric.closedBall a ε - Metric.ball b δ = Metric.ball (a - b) (ε + δ)

Tactic:
simp_rw [sub_eq_add_neg, neg_ball, closedBall_add_ball hε hδ]

Result:
no goals
-- Mathlib/Topology/UrysohnsLemma.lean
theorem approx_le_approx_of_U_sub_C {c₁ c₂ : CU P} (h : c₁.U ⊆ c₂.C) (n₁ n₂ : ℕ) (x : X) :
    c₂.approx n₂ x ≤ c₁.approx n₁ x

Proof state:
case neg
X : Type u_1
inst✝ : TopologicalSpace X
P : Set X → Prop
c₁ c₂ : CU P
h : c₁.U ⊆ c₂.C
n₁ n₂ : ℕ
x : X
hx : x ∉ c₁.U
⊢ approx n₂ c₂ x ≤ approx n₁ c₁ x

Tactic:
calc
  approx n₂ c₂ x ≤ 1 := approx_le_one _ _ _
  _ = approx n₁ c₁ x := (approx_of_nmem_U _ _ hx).symm

Result:
no goals

Proof state:
X : Type u_1
inst✝ : TopologicalSpace X
P : Set X → Prop
c₁ c₂ : CU P
h : c₁.U ⊆ c₂.C
n₁ n₂ : ℕ
x : X
⊢ approx n₂ c₂ x ≤ approx n₁ c₁ x

Tactic:
by_cases hx : x ∈ c₁.U

Result:
case pos
X : Type u_1
inst✝ : TopologicalSpace X
P : Set X → Prop
c₁ c₂ : CU P
h : c₁.U ⊆ c₂.C
n₁ n₂ : ℕ
x : X
hx : x ∈ c₁.U
⊢ approx n₂ c₂ x ≤ approx n₁ c₁ x

case neg
X : Type u_1
inst✝ : TopologicalSpace X
P : Set X → Prop
c₁ c₂ : CU P
h : c₁.U ⊆ c₂.C
n₁ n₂ : ℕ
x : X
hx : x ∉ c₁.U
⊢ approx n₂ c₂ x ≤ approx n₁ c₁ x

Proof state:
case pos
X : Type u_1
inst✝ : TopologicalSpace X
P : Set X → Prop
c₁ c₂ : CU P
h : c₁.U ⊆ c₂.C
n₁ n₂ : ℕ
x : X
hx : x ∈ c₁.U
⊢ approx n₂ c₂ x ≤ approx n₁ c₁ x

Tactic:
calc
  approx n₂ c₂ x = 0 := approx_of_mem_C _ _ (h hx)
  _ ≤ approx n₁ c₁ x := approx_nonneg _ _ _

Result:
no goals
-- Mathlib/RepresentationTheory/GroupCohomology/LowDegree.lean
theorem dZero_eq_zero [A.IsTrivial] : dZero A = 0

Proof state:
k G : Type u
inst✝² : CommRing k
inst✝¹ : Group G
A : Rep k G
inst✝ : A.IsTrivial
⊢ dZero A = 0

Tactic:
ext

Result:
case h.h
k G : Type u
inst✝² : CommRing k
inst✝¹ : Group G
A : Rep k G
inst✝ : A.IsTrivial
x✝¹ : ↑A.V
x✝ : G
⊢ (dZero A) x✝¹ x✝ = 0 x✝¹ x✝

Proof state:
case h.h
k G : Type u
inst✝² : CommRing k
inst✝¹ : Group G
A : Rep k G
inst✝ : A.IsTrivial
x✝¹ : ↑A.V
x✝ : G
⊢ (dZero A) x✝¹ x✝ = 0 x✝¹ x✝

Tactic:
simp only [dZero_apply, isTrivial_apply, sub_self, LinearMap.zero_apply, Pi.zero_apply]

Result:
no goals
-- Mathlib/Topology/UniformSpace/Basic.lean
theorem ball_entourageProd (u : Set (α × α)) (v : Set (β × β)) (x : α × β) :
    ball x (entourageProd u v) = ball x.1 u ×ˢ ball x.2 v

Proof state:
case h
α : Type ua
β : Type ub
u : Set (α × α)
v : Set (β × β)
x p : α × β
⊢ p ∈ ball x (entourageProd u v) ↔ p ∈ ball x.1 u ×ˢ ball x.2 v

Tactic:
simp only [ball, entourageProd, Set.mem_setOf_eq, Set.mem_prod, Set.mem_preimage]

Result:
no goals

Proof state:
α : Type ua
β : Type ub
u : Set (α × α)
v : Set (β × β)
x : α × β
⊢ ball x (entourageProd u v) = ball x.1 u ×ˢ ball x.2 v

Tactic:
ext p

Result:
case h
α : Type ua
β : Type ub
u : Set (α × α)
v : Set (β × β)
x p : α × β
⊢ p ∈ ball x (entourageProd u v) ↔ p ∈ ball x.1 u ×ˢ ball x.2 v
-- Mathlib/Combinatorics/SimpleGraph/IncMatrix.lean
theorem incMatrix_apply_mul_incMatrix_apply : G.incMatrix R a e * G.incMatrix R b e =
    (G.incidenceSet a ∩ G.incidenceSet b).indicator 1 e

Proof state:
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝ : MulZeroOneClass R
a b : α
e : Sym2 α
⊢ incMatrix R G a e * incMatrix R G b e = (G.incidenceSet a ∩ G.incidenceSet b).indicator 1 e

Tactic:
simp only [incMatrix, Set.indicator_apply, ite_zero_mul_ite_zero, Pi.one_apply, mul_one,
Set.mem_inter_iff]

Result:
no goals

Proof state:
R : Type u_1
α : Type u_2
G : SimpleGraph α
inst✝ : MulZeroOneClass R
a b : α
e : Sym2 α
⊢ incMatrix R G a e * incMatrix R G b e = (G.incidenceSet a ∩ G.incidenceSet b).indicator 1 e

Tactic:
classical simp only [incMatrix, Set.indicator_apply, ite_zero_mul_ite_zero, Pi.one_apply, mul_one,
  Set.mem_inter_iff]

Result:
no goals
-- Mathlib/Algebra/Ring/Periodic.lean
theorem Periodic.comp [Add α] (h : Periodic f c) (g : β → γ) : Periodic (g ∘ f) c

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
f : α → β
c : α
inst✝ : Add α
h : Periodic f c
g : β → γ
⊢ Periodic (g ∘ f) c

Tactic:
simp_all

Result:
no goals
-- Mathlib/Data/Set/Insert.lean
theorem disjoint_insert_left : Disjoint (insert a s) t ↔ a ∉ t ∧ Disjoint s t

Proof state:
α : Type u
s t : Set α
a : α
⊢ Disjoint (insert a s) t ↔ a ∉ t ∧ Disjoint s t

Tactic:
simp only [Set.disjoint_left, Set.mem_insert_iff, forall_eq_or_imp]

Result:
no goals
-- Mathlib/Analysis/Calculus/Deriv/Add.lean
theorem HasStrictDerivAt.const_sub (c : F) (hf : HasStrictDerivAt f f' x) :
    HasStrictDerivAt (fun x => c - f x) (-f') x

Proof state:
𝕜 : Type u
inst✝² : NontriviallyNormedField 𝕜
F : Type v
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : 𝕜 → F
f' : F
x : 𝕜
c : F
hf : HasStrictDerivAt f f' x
⊢ HasStrictDerivAt (fun x => c - f x) (-f') x

Tactic:
simpa only [sub_eq_add_neg] using hf.neg.const_add c

Result:
no goals
-- Mathlib/NumberTheory/ModularForms/JacobiTheta/OneVariable.lean
theorem jacobiTheta_T_sq_smul (τ : ℍ) : jacobiTheta (ModularGroup.T ^ 2 • τ :) = jacobiTheta τ

Proof state:
τ : ℍ
⊢ ↑(ModularGroup.T ^ 2 • τ) = 2 + ↑τ

Tactic:
have : ModularGroup.T ^ (2 : ℕ) = ModularGroup.T ^ (2 : ℤ) := rfl

Result:
τ : ℍ
this : ModularGroup.T ^ 2 = ModularGroup.T ^ 2
⊢ ↑(ModularGroup.T ^ 2 • τ) = 2 + ↑τ

Proof state:
τ : ℍ
this : ↑(ModularGroup.T ^ 2 • τ) = 2 + ↑τ
⊢ jacobiTheta ↑(ModularGroup.T ^ 2 • τ) = jacobiTheta ↑τ

Tactic:
simp_rw [this, jacobiTheta_two_add]

Result:
no goals

Proof state:
τ : ℍ
this : ModularGroup.T ^ 2 = ModularGroup.T ^ 2
⊢ ↑(ModularGroup.T ^ 2 • τ) = 2 + ↑τ

Tactic:
simp_rw [this, UpperHalfPlane.modular_T_zpow_smul, UpperHalfPlane.coe_vadd]

Result:
τ : ℍ
this : ModularGroup.T ^ 2 = ModularGroup.T ^ 2
⊢ ↑↑2 + ↑τ = 2 + ↑τ

Proof state:
τ : ℍ
⊢ jacobiTheta ↑(ModularGroup.T ^ 2 • τ) = jacobiTheta ↑τ

Tactic:
suffices (ModularGroup.T ^ 2 • τ :) = (2 : ℂ) + ↑τ by simp_rw [this, jacobiTheta_two_add]

Result:
τ : ℍ
⊢ ↑(ModularGroup.T ^ 2 • τ) = 2 + ↑τ

Proof state:
τ : ℍ
this : ModularGroup.T ^ 2 = ModularGroup.T ^ 2
⊢ ↑↑2 + ↑τ = 2 + ↑τ

Tactic:
norm_cast

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Restrict.lean
theorem restrict_iUnion_apply_ae [Countable ι] {s : ι → Set α} (hd : Pairwise (AEDisjoint μ on s))
    (hm : ∀ i, NullMeasurableSet (s i) μ) {t : Set α} (ht : MeasurableSet t) :
    μ.restrict (⋃ i, s i) t = ∑' i, μ.restrict (s i) t

Proof state:
α : Type u_2
ι : Type u_6
m0 : MeasurableSpace α
μ : Measure α
inst✝ : Countable ι
s : ι → Set α
hd : Pairwise (AEDisjoint μ on s)
hm : ∀ (i : ι), NullMeasurableSet (s i) μ
t : Set α
ht : MeasurableSet t
⊢ (μ.restrict (⋃ i, s i)) t = ∑' (i : ι), (μ.restrict (s i)) t

Tactic:
simp only [restrict_apply, ht, inter_iUnion]

Result:
α : Type u_2
ι : Type u_6
m0 : MeasurableSpace α
μ : Measure α
inst✝ : Countable ι
s : ι → Set α
hd : Pairwise (AEDisjoint μ on s)
hm : ∀ (i : ι), NullMeasurableSet (s i) μ
t : Set α
ht : MeasurableSet t
⊢ μ (⋃ i, t ∩ s i) = ∑' (i : ι), μ (t ∩ s i)

Proof state:
α : Type u_2
ι : Type u_6
m0 : MeasurableSpace α
μ : Measure α
inst✝ : Countable ι
s : ι → Set α
hd : Pairwise (AEDisjoint μ on s)
hm : ∀ (i : ι), NullMeasurableSet (s i) μ
t : Set α
ht : MeasurableSet t
⊢ μ (⋃ i, t ∩ s i) = ∑' (i : ι), μ (t ∩ s i)

Tactic:
exact
  measure_iUnion₀ (hd.mono fun i j h => h.mono inter_subset_right inter_subset_right)
    fun i => ht.nullMeasurableSet.inter (hm i)

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/Pullback/CommSq.lean
theorem isoPullback_hom_snd (h : IsPullback fst snd f g) [HasPullback f g] :
    h.isoPullback.hom ≫ pullback.snd _ _ = snd

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
inst✝ : HasPullback f g
⊢ h.isoPullback.hom ≫ pullback.snd f g = snd

Tactic:
dsimp [isoPullback, cone, CommSq.cone]

Result:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
inst✝ : HasPullback f g
⊢ (limit.isoLimitCone { cone := PullbackCone.mk fst snd ⋯, isLimit := h.isLimit }).inv ≫ pullback.snd f g = snd

Proof state:
C : Type u₁
inst✝¹ : Category.{v₁, u₁} C
P X Y Z : C
fst : P ⟶ X
snd : P ⟶ Y
f : X ⟶ Z
g : Y ⟶ Z
h : IsPullback fst snd f g
inst✝ : HasPullback f g
⊢ (limit.isoLimitCone { cone := PullbackCone.mk fst snd ⋯, isLimit := h.isLimit }).inv ≫ pullback.snd f g = snd

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/SpecificLimits/Normed.lean
theorem tendsto_self_mul_const_pow_of_lt_one {r : ℝ} (hr : 0 ≤ r) (h'r : r < 1) :
    Tendsto (fun n ↦ n * r ^ n : ℕ → ℝ) atTop (𝓝 0)

Proof state:
r : ℝ
hr : 0 ≤ r
h'r : r < 1
⊢ Tendsto (fun n => ↑n * r ^ n) atTop (𝓝 0)

Tactic:
simpa only [pow_one] using tendsto_pow_const_mul_const_pow_of_lt_one 1 hr h'r

Result:
no goals
-- Mathlib/RingTheory/PowerSeries/Basic.lean
theorem monomial_eq_mk (n : ℕ) (a : R) : monomial R n a = mk fun m => if m = n then a else 0 :=
  ext fun m => by rw [coeff_monomial, coeff_mk]

Proof state:
R : Type u_1
inst✝ : Semiring R
n : ℕ
a : R
m : ℕ
⊢ (coeff R m) ((monomial R n) a) = (coeff R m) (mk fun m => if m = n then a else 0)

Tactic:
rw [coeff_monomial, coeff_mk]

Result:
no goals
-- Mathlib/RingTheory/Ideal/Operations.lean
theorem eq_span_singleton_mul {x : R} (I J : Ideal R) :
    I = span {x} * J ↔ (∀ zI ∈ I, ∃ zJ ∈ J, x * zJ = zI) ∧ ∀ z ∈ J, x * z ∈ I

Proof state:
R : Type u
inst✝ : CommSemiring R
x : R
I J : Ideal R
⊢ I = span {x} * J ↔ (∀ zI ∈ I, ∃ zJ ∈ J, x * zJ = zI) ∧ ∀ z ∈ J, x * z ∈ I

Tactic:
simp only [le_antisymm_iff, le_span_singleton_mul_iff, span_singleton_mul_le_iff]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Matching.lean
lemma IsMatching.map_ofLE (h : M.IsMatching) (hGG' : G ≤ G') :
    (M.map (Hom.ofLE hGG')).IsMatching

Proof state:
case intro.intro.intro
V : Type u_1
G G' : SimpleGraph V
M : G.Subgraph
h : M.IsMatching
hGG' : G ≤ G'
v✝ : V
hv✝ : v✝ ∈ (Subgraph.map (Hom.ofLE hGG') M).verts
w✝ : V
hv : w✝ ∈ M.verts
hv' : (Hom.ofLE hGG') w✝ = v✝
w : V
hw : (fun w => M.Adj w✝ w) w ∧ ∀ (y : V), (fun w => M.Adj w✝ w) y → y = w
⊢ ∃! w, (Subgraph.map (Hom.ofLE hGG') M).Adj v✝ w

Tactic:
use w

Result:
case h
V : Type u_1
G G' : SimpleGraph V
M : G.Subgraph
h : M.IsMatching
hGG' : G ≤ G'
v✝ : V
hv✝ : v✝ ∈ (Subgraph.map (Hom.ofLE hGG') M).verts
w✝ : V
hv : w✝ ∈ M.verts
hv' : (Hom.ofLE hGG') w✝ = v✝
w : V
hw : (fun w => M.Adj w✝ w) w ∧ ∀ (y : V), (fun w => M.Adj w✝ w) y → y = w
⊢ (fun w => (Subgraph.map (Hom.ofLE hGG') M).Adj v✝ w) w ∧
    ∀ (y : V), (fun w => (Subgraph.map (Hom.ofLE hGG') M).Adj v✝ w) y → y = w

Proof state:
case h
V : Type u_1
G G' : SimpleGraph V
M : G.Subgraph
h : M.IsMatching
hGG' : G ≤ G'
v✝ : V
hv✝ : v✝ ∈ (Subgraph.map (Hom.ofLE hGG') M).verts
w✝ : V
hv : w✝ ∈ M.verts
hv' : (Hom.ofLE hGG') w✝ = v✝
w : V
hw : (fun w => M.Adj w✝ w) w ∧ ∀ (y : V), (fun w => M.Adj w✝ w) y → y = w
⊢ (fun w => (Subgraph.map (Hom.ofLE hGG') M).Adj v✝ w) w ∧
    ∀ (y : V), (fun w => (Subgraph.map (Hom.ofLE hGG') M).Adj v✝ w) y → y = w

Tactic:
simpa using hv' ▸ hw

Result:
no goals

Proof state:
V : Type u_1
G G' : SimpleGraph V
M : G.Subgraph
h : M.IsMatching
hGG' : G ≤ G'
⊢ (Subgraph.map (Hom.ofLE hGG') M).IsMatching

Tactic:
intro _ hv

Result:
V : Type u_1
G G' : SimpleGraph V
M : G.Subgraph
h : M.IsMatching
hGG' : G ≤ G'
v✝ : V
hv : v✝ ∈ (Subgraph.map (Hom.ofLE hGG') M).verts
⊢ ∃! w, (Subgraph.map (Hom.ofLE hGG') M).Adj v✝ w

Proof state:
case intro.intro
V : Type u_1
G G' : SimpleGraph V
M : G.Subgraph
h : M.IsMatching
hGG' : G ≤ G'
v✝ : V
hv✝ : v✝ ∈ (Subgraph.map (Hom.ofLE hGG') M).verts
w✝ : V
hv : w✝ ∈ M.verts
hv' : (Hom.ofLE hGG') w✝ = v✝
⊢ ∃! w, (Subgraph.map (Hom.ofLE hGG') M).Adj v✝ w

Tactic:
obtain ⟨w, hw⟩ := h hv

Result:
case intro.intro.intro
V : Type u_1
G G' : SimpleGraph V
M : G.Subgraph
h : M.IsMatching
hGG' : G ≤ G'
v✝ : V
hv✝ : v✝ ∈ (Subgraph.map (Hom.ofLE hGG') M).verts
w✝ : V
hv : w✝ ∈ M.verts
hv' : (Hom.ofLE hGG') w✝ = v✝
w : V
hw : (fun w => M.Adj w✝ w) w ∧ ∀ (y : V), (fun w => M.Adj w✝ w) y → y = w
⊢ ∃! w, (Subgraph.map (Hom.ofLE hGG') M).Adj v✝ w

Proof state:
V : Type u_1
G G' : SimpleGraph V
M : G.Subgraph
h : M.IsMatching
hGG' : G ≤ G'
v✝ : V
hv : v✝ ∈ (Subgraph.map (Hom.ofLE hGG') M).verts
⊢ ∃! w, (Subgraph.map (Hom.ofLE hGG') M).Adj v✝ w

Tactic:
obtain ⟨_, hv, hv'⟩ := Set.mem_image _ _ _ |>.mp hv

Result:
case intro.intro
V : Type u_1
G G' : SimpleGraph V
M : G.Subgraph
h : M.IsMatching
hGG' : G ≤ G'
v✝ : V
hv✝ : v✝ ∈ (Subgraph.map (Hom.ofLE hGG') M).verts
w✝ : V
hv : w✝ ∈ M.verts
hv' : (Hom.ofLE hGG') w✝ = v✝
⊢ ∃! w, (Subgraph.map (Hom.ofLE hGG') M).Adj v✝ w
-- Mathlib/Algebra/Polynomial/GroupRingAction.lean
theorem prodXSubSMul.eval (x : R) : (prodXSubSMul G R x).eval x = 0 :=
  letI := Classical.decEq R
  (map_prod ((Polynomial.aeval x).toRingHom.toMonoidHom : R[X] →* R) _ _).trans <|
    Finset.prod_eq_zero (Finset.mem_univ <| QuotientGroup.mk 1) <| by simp

Proof state:
G : Type u_2
inst✝³ : Group G
inst✝² : Fintype G
R : Type u_3
inst✝¹ : CommRing R
inst✝ : MulSemiringAction G R
x : R
this : DecidableEq R := Classical.decEq R
⊢ ↑(aeval x).toRingHom (X - C (ofQuotientStabilizer G x ↑1)) = 0

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/Convex/Slope.lean
theorem concaveOn_of_slope_anti_adjacent (hs : Convex 𝕜 s)
    (hf :
      ∀ {x y z : 𝕜},
        x ∈ s → z ∈ s → x < y → y < z → (f z - f y) / (z - y) ≤ (f y - f x) / (y - x)) :
    ConcaveOn 𝕜 s f

Proof state:
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hs : Convex 𝕜 s
hf : ∀ {x y z : 𝕜}, x ∈ s → z ∈ s → x < y → y < z → (f z - f y) / (z - y) ≤ (f y - f x) / (y - x)
⊢ ConcaveOn 𝕜 s f

Tactic:
rw [← neg_convexOn_iff]

Result:
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hs : Convex 𝕜 s
hf : ∀ {x y z : 𝕜}, x ∈ s → z ∈ s → x < y → y < z → (f z - f y) / (z - y) ≤ (f y - f x) / (y - x)
⊢ ConvexOn 𝕜 s (-f)

Proof state:
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hs : Convex 𝕜 s
hf : ∀ {x y z : 𝕜}, x ∈ s → z ∈ s → x < y → y < z → (f z - f y) / (z - y) ≤ (f y - f x) / (y - x)
x✝ y✝ z✝ : 𝕜
hx : x✝ ∈ s
hz : z✝ ∈ s
hxy : x✝ < y✝
hyz : y✝ < z✝
⊢ -(((-f) z✝ - (-f) y✝) / (z✝ - y✝)) ≤ -(((-f) y✝ - (-f) x✝) / (y✝ - x✝))

Tactic:
simp_rw [← neg_div, neg_sub, Pi.neg_apply, neg_sub_neg]

Result:
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hs : Convex 𝕜 s
hf : ∀ {x y z : 𝕜}, x ∈ s → z ∈ s → x < y → y < z → (f z - f y) / (z - y) ≤ (f y - f x) / (y - x)
x✝ y✝ z✝ : 𝕜
hx : x✝ ∈ s
hz : z✝ ∈ s
hxy : x✝ < y✝
hyz : y✝ < z✝
⊢ (f z✝ - f y✝) / (z✝ - y✝) ≤ (f y✝ - f x✝) / (y✝ - x✝)

Proof state:
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hs : Convex 𝕜 s
hf : ∀ {x y z : 𝕜}, x ∈ s → z ∈ s → x < y → y < z → (f z - f y) / (z - y) ≤ (f y - f x) / (y - x)
x✝ y✝ z✝ : 𝕜
hx : x✝ ∈ s
hz : z✝ ∈ s
hxy : x✝ < y✝
hyz : y✝ < z✝
⊢ ((-f) y✝ - (-f) x✝) / (y✝ - x✝) ≤ ((-f) z✝ - (-f) y✝) / (z✝ - y✝)

Tactic:
rw [← neg_le_neg_iff]

Result:
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hs : Convex 𝕜 s
hf : ∀ {x y z : 𝕜}, x ∈ s → z ∈ s → x < y → y < z → (f z - f y) / (z - y) ≤ (f y - f x) / (y - x)
x✝ y✝ z✝ : 𝕜
hx : x✝ ∈ s
hz : z✝ ∈ s
hxy : x✝ < y✝
hyz : y✝ < z✝
⊢ -(((-f) z✝ - (-f) y✝) / (z✝ - y✝)) ≤ -(((-f) y✝ - (-f) x✝) / (y✝ - x✝))

Proof state:
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hs : Convex 𝕜 s
hf : ∀ {x y z : 𝕜}, x ∈ s → z ∈ s → x < y → y < z → (f z - f y) / (z - y) ≤ (f y - f x) / (y - x)
x✝ y✝ z✝ : 𝕜
hx : x✝ ∈ s
hz : z✝ ∈ s
hxy : x✝ < y✝
hyz : y✝ < z✝
⊢ (f z✝ - f y✝) / (z✝ - y✝) ≤ (f y✝ - f x✝) / (y✝ - x✝)

Tactic:
exact hf hx hz hxy hyz

Result:
no goals

Proof state:
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hs : Convex 𝕜 s
hf : ∀ {x y z : 𝕜}, x ∈ s → z ∈ s → x < y → y < z → (f z - f y) / (z - y) ≤ (f y - f x) / (y - x)
⊢ ConvexOn 𝕜 s (-f)

Tactic:
refine convexOn_of_slope_mono_adjacent hs fun hx hz hxy hyz => ?_

Result:
𝕜 : Type u_1
inst✝ : LinearOrderedField 𝕜
s : Set 𝕜
f : 𝕜 → 𝕜
hs : Convex 𝕜 s
hf : ∀ {x y z : 𝕜}, x ∈ s → z ∈ s → x < y → y < z → (f z - f y) / (z - y) ≤ (f y - f x) / (y - x)
x✝ y✝ z✝ : 𝕜
hx : x✝ ∈ s
hz : z✝ ∈ s
hxy : x✝ < y✝
hyz : y✝ < z✝
⊢ ((-f) y✝ - (-f) x✝) / (y✝ - x✝) ≤ ((-f) z✝ - (-f) y✝) / (z✝ - y✝)
-- Mathlib/.lake/packages/lean4/src/lean/Std/Sat/AIG/RefVec.lean
theorem get_push_ref_eq (s : RefVec aig len) (ref : AIG.Ref aig) :
    (s.push ref).get len (by omega) = ref

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
len : Nat
s : aig.RefVec len
ref : aig.Ref
this : s.refs.size = len
⊢ (s.push ref).get len ⋯ = ref

Tactic:
simp [get, push, ← this]

Result:
no goals

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
len : Nat
s : aig.RefVec len
ref : aig.Ref
⊢ len < len + 1

Tactic:
omega

Result:
no goals

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
len : Nat
s : aig.RefVec len
ref : aig.Ref
⊢ (s.push ref).get len ⋯ = ref

Tactic:
have := s.hlen

Result:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
aig : AIG α
len : Nat
s : aig.RefVec len
ref : aig.Ref
this : s.refs.size = len
⊢ (s.push ref).get len ⋯ = ref