harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/RingTheory/Multiplicity.lean
theorem finiteMultiplicity_of_emultiplicity_eq_natCast {n : ℕ} (h : emultiplicity a b = n) :
    FiniteMultiplicity a b

Proof state:
α : Type u_1
inst✝ : Monoid α
a b : α
n : ℕ
h : emultiplicity a b = ↑n
nh : ¬FiniteMultiplicity a b
⊢ False

Tactic:
rw [← emultiplicity_eq_top, h] at nh

Result:
α : Type u_1
inst✝ : Monoid α
a b : α
n : ℕ
h : emultiplicity a b = ↑n
nh : ↑n = ⊤
⊢ False

Proof state:
α : Type u_1
inst✝ : Monoid α
a b : α
n : ℕ
h : emultiplicity a b = ↑n
nh : ↑n = ⊤
⊢ False

Tactic:
trivial

Result:
no goals

Proof state:
α : Type u_1
inst✝ : Monoid α
a b : α
n : ℕ
h : emultiplicity a b = ↑n
⊢ FiniteMultiplicity a b

Tactic:
by_contra! nh

Result:
α : Type u_1
inst✝ : Monoid α
a b : α
n : ℕ
h : emultiplicity a b = ↑n
nh : ¬FiniteMultiplicity a b
⊢ False
-- Mathlib/LinearAlgebra/Dual.lean
theorem dualMap_surjective_iff {f : V₁ →ₗ[K] V₂} :
    Function.Surjective f.dualMap ↔ Function.Injective f

Proof state:
K : Type uK
inst✝⁴ : Field K
V₁ : Type uV₁
V₂ : Type uV₂
inst✝³ : AddCommGroup V₁
inst✝² : Module K V₁
inst✝¹ : AddCommGroup V₂
inst✝ : Module K V₂
f : V₁ →ₗ[K] V₂
⊢ Function.Surjective ⇑f.dualMap ↔ Function.Injective ⇑f

Tactic:
rw [← LinearMap.range_eq_top, range_dualMap_eq_dualAnnihilator_ker,
    ← Submodule.dualAnnihilator_bot, Subspace.dualAnnihilator_inj, LinearMap.ker_eq_bot]

Result:
no goals
-- Mathlib/Algebra/Category/ModuleCat/Monoidal/Basic.lean
/-- Extensionality lemma for morphisms from a module of the form `M₁ ⊗ (M₂ ⊗ M₃)`. -/
lemma tensor_ext₃ {f g : M₁ ⊗ (M₂ ⊗ M₃) ⟶ M₄}
    (h : ∀ m₁ m₂ m₃, f (m₁ ⊗ₜ (m₂ ⊗ₜ m₃)) = g (m₁ ⊗ₜ (m₂ ⊗ₜ m₃))) :
    f = g

Proof state:
R : Type u
inst✝ : CommRing R
M₁ M₂ M₃ M₄ : ModuleCat R
f g : M₁ ⊗ M₂ ⊗ M₃ ⟶ M₄
h :
  ∀ (m₁ : ↑M₁) (m₂ : ↑M₂) (m₃ : ↑M₃),
    (ConcreteCategory.hom f) (m₁ ⊗ₜ[R] m₂ ⊗ₜ[R] m₃) = (ConcreteCategory.hom g) (m₁ ⊗ₜ[R] m₂ ⊗ₜ[R] m₃)
⊢ f = g

Tactic:
rw [← cancel_epi (α_ _ _ _).hom]

Result:
R : Type u
inst✝ : CommRing R
M₁ M₂ M₃ M₄ : ModuleCat R
f g : M₁ ⊗ M₂ ⊗ M₃ ⟶ M₄
h :
  ∀ (m₁ : ↑M₁) (m₂ : ↑M₂) (m₃ : ↑M₃),
    (ConcreteCategory.hom f) (m₁ ⊗ₜ[R] m₂ ⊗ₜ[R] m₃) = (ConcreteCategory.hom g) (m₁ ⊗ₜ[R] m₂ ⊗ₜ[R] m₃)
⊢ (α_ M₁ M₂ M₃).hom ≫ f = (α_ M₁ M₂ M₃).hom ≫ g

Proof state:
R : Type u
inst✝ : CommRing R
M₁ M₂ M₃ M₄ : ModuleCat R
f g : M₁ ⊗ M₂ ⊗ M₃ ⟶ M₄
h :
  ∀ (m₁ : ↑M₁) (m₂ : ↑M₂) (m₃ : ↑M₃),
    (ConcreteCategory.hom f) (m₁ ⊗ₜ[R] m₂ ⊗ₜ[R] m₃) = (ConcreteCategory.hom g) (m₁ ⊗ₜ[R] m₂ ⊗ₜ[R] m₃)
⊢ (α_ M₁ M₂ M₃).hom ≫ f = (α_ M₁ M₂ M₃).hom ≫ g

Tactic:
exact tensor_ext₃' h

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Attach.lean
theorem unattach_attach {l : Vector α n} : l.attach.unattach = l

Proof state:
case mk
α : Type u_1
l : Array α
⊢ { toArray := l, size_toArray := ⋯ }.attach.unattach = { toArray := l, size_toArray := ⋯ }

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
n : Nat
l : Vector α n
⊢ l.attach.unattach = l

Tactic:
rcases l with ⟨l, rfl⟩

Result:
case mk
α : Type u_1
l : Array α
⊢ { toArray := l, size_toArray := ⋯ }.attach.unattach = { toArray := l, size_toArray := ⋯ }
-- Mathlib/Order/UpperLower/Basic.lean
theorem UpperSet.iInf_Ici (s : Set α) : ⨅ a ∈ s, UpperSet.Ici a = upperClosure s

Proof state:
case a.h
α : Type u_1
inst✝ : Preorder α
s : Set α
x✝ : α
⊢ x✝ ∈ ↑(⨅ a ∈ s, Ici a) ↔ x✝ ∈ ↑(upperClosure s)

Tactic:
simp

Result:
no goals

Proof state:
α : Type u_1
inst✝ : Preorder α
s : Set α
⊢ ⨅ a ∈ s, Ici a = upperClosure s

Tactic:
ext

Result:
case a.h
α : Type u_1
inst✝ : Preorder α
s : Set α
x✝ : α
⊢ x✝ ∈ ↑(⨅ a ∈ s, Ici a) ↔ x✝ ∈ ↑(upperClosure s)
-- Mathlib/AlgebraicGeometry/EllipticCurve/DivisionPolynomial/Basic.lean
lemma ΨSq_even_ofNat (m : ℕ) : W.ΨSq (2 * (m + 3)) =
    (W.preΨ' (m + 2) ^ 2 * W.preΨ' (m + 3) * W.preΨ' (m + 5) -
      W.preΨ' (m + 1) * W.preΨ' (m + 3) * W.preΨ' (m + 4) ^ 2) ^ 2 * W.Ψ₂Sq

Proof state:
R : Type r
inst✝ : CommRing R
W : WeierstrassCurve R
m : ℕ
⊢ W.ΨSq (2 * (↑m + 3)) =
    (W.preΨ' (m + 2) ^ 2 * W.preΨ' (m + 3) * W.preΨ' (m + 5) -
          W.preΨ' (m + 1) * W.preΨ' (m + 3) * W.preΨ' (m + 4) ^ 2) ^
        2 *
      W.Ψ₂Sq

Tactic:
rw_mod_cast [ΨSq_ofNat, preΨ'_even, if_pos <| even_two_mul _]

Result:
no goals
-- Mathlib/RingTheory/Coprime/Basic.lean
theorem mul_add_left_left {x y : R} (h : IsCoprime x y) (z : R) : IsCoprime (y * z + x) y

Proof state:
R : Type u
inst✝ : CommRing R
x y : R
h : IsCoprime x y
z : R
⊢ IsCoprime (y * z + x) y

Tactic:
rw [add_comm]

Result:
R : Type u
inst✝ : CommRing R
x y : R
h : IsCoprime x y
z : R
⊢ IsCoprime (x + y * z) y

Proof state:
R : Type u
inst✝ : CommRing R
x y : R
h : IsCoprime x y
z : R
⊢ IsCoprime (x + y * z) y

Tactic:
exact h.add_mul_left_left z

Result:
no goals
-- Mathlib/RingTheory/Ideal/Span.lean
theorem span_pair_comm {x y : α} : (span {x, y} : Ideal α) = span {y, x}

Proof state:
α : Type u
inst✝ : Semiring α
x y : α
⊢ span {x, y} = span {y, x}

Tactic:
simp only [span_insert, sup_comm]

Result:
no goals
-- Mathlib/Analysis/Calculus/FDeriv/Add.lean
theorem fderiv_const_add (c : F) : fderiv 𝕜 (fun y => c + f y) x = fderiv 𝕜 f x

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type u_2
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
F : Type u_3
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
f : E → F
x : E
c : F
⊢ fderiv 𝕜 (fun y => c + f y) x = fderiv 𝕜 f x

Tactic:
simp only [add_comm c, fderiv_add_const]

Result:
no goals
-- Mathlib/CategoryTheory/Subobject/Limits.lean
theorem imageSubobject_iso_comp [HasEqualizers C] {X' : C} (h : X' ⟶ X) [IsIso h] (f : X ⟶ Y)
    [HasImage f] : imageSubobject (h ≫ f) = imageSubobject f :=
  le_antisymm (imageSubobject_comp_le h f)
    (Subobject.mk_le_mk_of_comm (inv (image.preComp h f)) (by simp))

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
X Y : C
inst✝² : HasEqualizers C
X' : C
h : X' ⟶ X
inst✝¹ : IsIso h
f : X ⟶ Y
inst✝ : HasImage f
⊢ inv (image.preComp h f) ≫ image.ι (h ≫ f) = image.ι f

Tactic:
simp

Result:
no goals
-- Mathlib/RingTheory/Int/Basic.lean
theorem gcd_ne_one_iff_gcd_mul_right_ne_one {a : ℤ} {m n : ℕ} :
    a.gcd (m * n) ≠ 1 ↔ a.gcd m ≠ 1 ∨ a.gcd n ≠ 1

Proof state:
a : ℤ
m n : ℕ
⊢ a.gcd (↑m * ↑n) ≠ 1 ↔ a.gcd ↑m ≠ 1 ∨ a.gcd ↑n ≠ 1

Tactic:
simp only [← isCoprime_iff_gcd_eq_one, ← not_and_or, not_iff_not, IsCoprime.mul_right_iff]

Result:
no goals
-- Mathlib/Algebra/Group/Commute/Basic.lean
theorem div_mul_div_comm (hbd : Commute b d) (hbc : Commute b⁻¹ c) :
    a / b * (c / d) = a * c / (b * d)

Proof state:
G : Type u_1
inst✝ : DivisionMonoid G
a b c d : G
hbd : Commute b d
hbc : Commute b⁻¹ c
⊢ a / b * (c / d) = a * c / (b * d)

Tactic:
simp_rw [div_eq_mul_inv, mul_inv_rev, hbd.inv_inv.symm.eq, hbc.mul_mul_mul_comm]

Result:
no goals
-- Mathlib/.lake/packages/batteries/Batteries/Data/Range/Lemmas.lean
theorem size_stop_le_start : ∀ r : Range, r.stop ≤ r.start → r.size = 0
  | ⟨start, stop, step, _⟩, h => by
    simp_all [size, Nat.div_eq_zero_iff_lt]
    omega

Proof state:
start stop step : Nat
step_pos✝ : 0 < step
h :
  { start := start, stop := stop, step := step, step_pos := step_pos✝ }.stop ≤
    { start := start, stop := stop, step := step, step_pos := step_pos✝ }.start
⊢ { start := start, stop := stop, step := step, step_pos := step_pos✝ }.size = 0

Tactic:
simp_all [size, Nat.div_eq_zero_iff_lt]

Result:
start stop step : Nat
step_pos✝ : 0 < step
h : stop ≤ start
⊢ stop - start + step - 1 < step

Proof state:
start stop step : Nat
step_pos✝ : 0 < step
h : stop ≤ start
⊢ stop - start + step - 1 < step

Tactic:
omega

Result:
no goals
-- Mathlib/Topology/FiberBundle/Trivialization.lean
theorem mem_source : x ∈ e.source ↔ proj x ∈ e.baseSet

Proof state:
B : Type u_1
F : Type u_2
Z : Type u_4
inst✝¹ : TopologicalSpace B
inst✝ : TopologicalSpace F
proj : Z → B
e : Pretrivialization F proj
x : Z
⊢ x ∈ e.source ↔ proj x ∈ e.baseSet

Tactic:
rw [e.source_eq, mem_preimage]

Result:
no goals
-- Mathlib/RingTheory/Derivation/Basic.lean
theorem eqOn_adjoin {s : Set A} (h : Set.EqOn D1 D2 s) : Set.EqOn D1 D2 (adjoin R s) := fun _ hx =>
  Algebra.adjoin_induction (hx := hx) h
    (fun r => (D1.map_algebraMap r).trans (D2.map_algebraMap r).symm)
    (fun x y _ _ hx hy => by simp only [map_add, *]) fun x y _ _ hx hy => by simp only [leibniz, *]

Proof state:
R : Type u_1
A : Type u_2
M : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring A
inst✝³ : AddCommMonoid M
inst✝² : Algebra R A
inst✝¹ : Module A M
inst✝ : Module R M
D1 D2 : Derivation R A M
s : Set A
h : Set.EqOn (⇑D1) (⇑D2) s
x✝² : A
hx✝ : x✝² ∈ ↑(adjoin R s)
x y : A
x✝¹ : x ∈ adjoin R s
x✝ : y ∈ adjoin R s
hx : D1 x = D2 x
hy : D1 y = D2 y
⊢ D1 (x * y) = D2 (x * y)

Tactic:
simp only [leibniz, *]

Result:
no goals

Proof state:
R : Type u_1
A : Type u_2
M : Type u_4
inst✝⁵ : CommSemiring R
inst✝⁴ : CommSemiring A
inst✝³ : AddCommMonoid M
inst✝² : Algebra R A
inst✝¹ : Module A M
inst✝ : Module R M
D1 D2 : Derivation R A M
s : Set A
h : Set.EqOn (⇑D1) (⇑D2) s
x✝² : A
hx✝ : x✝² ∈ ↑(adjoin R s)
x y : A
x✝¹ : x ∈ adjoin R s
x✝ : y ∈ adjoin R s
hx : D1 x = D2 x
hy : D1 y = D2 y
⊢ D1 (x + y) = D2 (x + y)

Tactic:
simp only [map_add, *]

Result:
no goals
-- Mathlib/MeasureTheory/Function/ConditionalExpectation/AEMeasurable.lean
theorem isometry_lpMeasSubgroupToLpTrim [hp : Fact (1 ≤ p)] (hm : m ≤ m0) :
    Isometry (lpMeasSubgroupToLpTrim F p μ hm) :=
  Isometry.of_dist_eq fun f g => by
    rw [dist_eq_norm, ← lpMeasSubgroupToLpTrim_sub, lpMeasSubgroupToLpTrim_norm_map,
      dist_eq_norm]

Proof state:
α : Type u_1
F : Type u_2
p : ℝ≥0∞
inst✝ : NormedAddCommGroup F
m m0 : MeasurableSpace α
μ : Measure α
hp : Fact (1 ≤ p)
hm : m ≤ m0
f g : ↥(lpMeasSubgroup F m p μ)
⊢ dist (lpMeasSubgroupToLpTrim F p μ hm f) (lpMeasSubgroupToLpTrim F p μ hm g) = dist f g

Tactic:
rw [dist_eq_norm, ← lpMeasSubgroupToLpTrim_sub, lpMeasSubgroupToLpTrim_norm_map,
  dist_eq_norm]

Result:
no goals
-- Mathlib/Algebra/GroupWithZero/Units/Basic.lean
theorem div_eq_zero_iff : a / b = 0 ↔ a = 0 ∨ b = 0

Proof state:
G₀ : Type u_3
inst✝ : GroupWithZero G₀
a b : G₀
⊢ a / b = 0 ↔ a = 0 ∨ b = 0

Tactic:
simp [div_eq_mul_inv]

Result:
no goals
-- Mathlib/Order/Lattice.lean
theorem inf_left_idem (a b : α) : a ⊓ (a ⊓ b) = a ⊓ b

Proof state:
α : Type u
inst✝ : SemilatticeInf α
a b : α
⊢ a ⊓ (a ⊓ b) = a ⊓ b

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/Normed/Group/Basic.lean
@[simp, norm_cast] lemma enorm_lt_coe : ‖x‖ₑ < r ↔ ‖x‖₊ < r

Proof state:
E : Type u_8
inst✝ : NNNorm E
x : E
r : ℝ≥0
⊢ ‖x‖ₑ < ↑r ↔ ‖x‖₊ < r

Tactic:
simp [enorm]

Result:
no goals
-- Mathlib/CategoryTheory/Sites/Subcanonical.lean
/-- Variant of `map_yonedaEquiv` with general `g`. This is technically strictly more general
    than `map_yonedaEquiv`, but `map_yonedaEquiv` is sometimes preferable because it
    can avoid the "motive is not type correct" error. -/
lemma map_yonedaULiftEquiv' {X Y : Cᵒᵖ} {F : Sheaf J (Type (max v v'))}
    (f : J.yonedaULift.obj (unop X) ⟶ F)
    (g : X ⟶ Y) : F.val.map g (J.yonedaULiftEquiv f) = f.val.app Y ⟨g.unop⟩

Proof state:
C : Type u
inst✝¹ : Category.{v, u} C
J : GrothendieckTopology C
inst✝ : J.Subcanonical
X Y : Cᵒᵖ
F : Sheaf J (Type (max v v'))
f : (yonedaULift.{v', v, u} J).obj (unop X) ⟶ F
g : X ⟶ Y
⊢ F.val.map g (J.yonedaULiftEquiv f) = f.val.app Y { down := g.unop }

Tactic:
rw [yonedaULiftEquiv_naturality', yonedaULiftEquiv_comp, yonedaULiftEquiv_yonedaULift_map]

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Oriented/Affine.lean
theorem angle_eq_pi_div_two_of_oangle_eq_pi_div_two {p₁ p₂ p₃ : P} (h : ∡ p₁ p₂ p₃ = ↑(π / 2)) :
    ∠ p₁ p₂ p₃ = π / 2

Proof state:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ = ↑(π / 2)
⊢ ∠ p₁ p₂ p₃ = π / 2

Tactic:
rw [angle, ← InnerProductGeometry.inner_eq_zero_iff_angle_eq_pi_div_two]

Result:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ = ↑(π / 2)
⊢ inner (p₁ -ᵥ p₂) (p₃ -ᵥ p₂) = 0

Proof state:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : ∡ p₁ p₂ p₃ = ↑(π / 2)
⊢ inner (p₁ -ᵥ p₂) (p₃ -ᵥ p₂) = 0

Tactic:
exact o.inner_eq_zero_of_oangle_eq_pi_div_two h

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/BinaryEntropy.lean
@[simp] lemma qaryEntropy_two : qaryEntropy 2 = binEntropy

Proof state:
⊢ qaryEntropy 2 = binEntropy

Tactic:
ext

Result:
case h
x✝ : ℝ
⊢ qaryEntropy 2 x✝ = binEntropy x✝

Proof state:
case h
x✝ : ℝ
⊢ qaryEntropy 2 x✝ = binEntropy x✝

Tactic:
simp [qaryEntropy]

Result:
no goals
-- Mathlib/Data/DFinsupp/NeLocus.lean
theorem neLocus_sub_right : neLocus (f₁ - g) (f₂ - g) = neLocus f₁ f₂

Proof state:
α : Type u_1
N : α → Type u_2
inst✝² : DecidableEq α
inst✝¹ : (a : α) → DecidableEq (N a)
inst✝ : (a : α) → AddGroup (N a)
f₁ f₂ g : Π₀ (a : α), N a
⊢ (f₁ - g).neLocus (f₂ - g) = f₁.neLocus f₂

Tactic:
simpa only [sub_eq_add_neg] using @neLocus_add_right α N _ _ _ _ _ _

Result:
no goals
-- Mathlib/GroupTheory/GroupAction/SubMulAction.lean
theorem stabilizer_of_subMul.submonoid {p : SubMulAction R M} (m : p) :
    MulAction.stabilizerSubmonoid R m = MulAction.stabilizerSubmonoid R (m : M)

Proof state:
R : Type u
M : Type v
inst✝¹ : Monoid R
inst✝ : MulAction R M
p : SubMulAction R M
m : ↥p
⊢ MulAction.stabilizerSubmonoid R m = MulAction.stabilizerSubmonoid R ↑m

Tactic:
ext

Result:
case h
R : Type u
M : Type v
inst✝¹ : Monoid R
inst✝ : MulAction R M
p : SubMulAction R M
m : ↥p
x✝ : R
⊢ x✝ ∈ MulAction.stabilizerSubmonoid R m ↔ x✝ ∈ MulAction.stabilizerSubmonoid R ↑m

Proof state:
case h
R : Type u
M : Type v
inst✝¹ : Monoid R
inst✝ : MulAction R M
p : SubMulAction R M
m : ↥p
x✝ : R
⊢ x✝ ∈ MulAction.stabilizerSubmonoid R m ↔ x✝ ∈ MulAction.stabilizerSubmonoid R ↑m

Tactic:
simp only [MulAction.mem_stabilizerSubmonoid_iff, ← SubMulAction.val_smul, SetLike.coe_eq_coe]

Result:
no goals
-- Mathlib/CategoryTheory/Monoidal/Preadditive.lean
theorem add_tensor {W X Y Z : C} (f g : W ⟶ X) (h : Y ⟶ Z) : (f + g) ⊗ h = f ⊗ h + g ⊗ h

Proof state:
C : Type u_1
inst✝³ : Category.{u_2, u_1} C
inst✝² : Preadditive C
inst✝¹ : MonoidalCategory C
inst✝ : MonoidalPreadditive C
W X Y Z : C
f g : W ⟶ X
h : Y ⟶ Z
⊢ (f + g) ⊗ h = f ⊗ h + g ⊗ h

Tactic:
simp [tensorHom_def]

Result:
no goals
-- Mathlib/CategoryTheory/Localization/Monoidal.lean
@[reassoc]
lemma whisker_exchange {Q X Y Z : LocalizedMonoidal L W ε} (f : Q ⟶ X) (g : Y ⟶ Z) :
    Q ◁ g ≫ f ▷ Z = f ▷ Y ≫ X ◁ g

Proof state:
C : Type u_1
D : Type u_2
inst✝⁴ : Category.{u_3, u_1} C
inst✝³ : Category.{u_4, u_2} D
L : C ⥤ D
W : MorphismProperty C
inst✝² : MonoidalCategory C
inst✝¹ : W.IsMonoidal
inst✝ : L.IsLocalization W
unit : D
ε : L.obj (𝟙_ C) ≅ unit
Q X Y Z : LocalizedMonoidal L W ε
f : Q ⟶ X
g : Y ⟶ Z
⊢ Q ◁ g ≫ f ▷ Z = f ▷ Y ≫ X ◁ g

Tactic:
simp only [← id_tensorHom, ← tensorHom_id, ← tensor_comp, id_comp, comp_id]

Result:
no goals
-- Mathlib/Data/Seq/WSeq.lean
theorem exists_of_mem_bind {s : WSeq α} {f : α → WSeq β} {b} (h : b ∈ bind s f) :
    ∃ a ∈ s, b ∈ f a :=
  let ⟨t, tm, bt⟩ := exists_of_mem_join h
  let ⟨a, as, e⟩ := exists_of_mem_map tm
  ⟨a, as, by rwa [e]⟩

Proof state:
α : Type u
β : Type v
s : WSeq α
f : α → WSeq β
b : β
h : b ∈ s.bind f
t : WSeq β
tm : t ∈ map f s
bt : b ∈ t
a : α
as : a ∈ s
e : f a = t
⊢ b ∈ f a

Tactic:
rwa [e]

Result:
no goals
-- Mathlib/RingTheory/Ideal/Maps.lean
theorem map_of_equiv {I : Ideal R} (f : R ≃+* S) :
    (I.map (f : R →+* S)).map (f.symm : S →+* R) = I

Proof state:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
I : Ideal R
f : R ≃+* S
⊢ map (↑f.symm) (map (↑f) I) = I

Tactic:
rw [← RingEquiv.toRingHom_eq_coe, ← RingEquiv.toRingHom_eq_coe, map_map,
  RingEquiv.toRingHom_eq_coe, RingEquiv.toRingHom_eq_coe, RingEquiv.symm_comp, map_id]

Result:
no goals
-- Mathlib/Algebra/Ring/Int/Units.lean
lemma units_eq_one_or (u : ℤˣ) : u = 1 ∨ u = -1

Proof state:
u : ℤˣ
⊢ u = 1 ∨ u = -1

Tactic:
simpa only [Units.ext_iff] using isUnit_eq_one_or u.isUnit

Result:
no goals
-- Mathlib/Analysis/MeanInequalities.lean
theorem young_inequality_real (a b : ℝ≥0) {p q : ℝ} (hpq : p.IsConjExponent q) :
    a * b ≤ a ^ p / Real.toNNReal p + b ^ q / Real.toNNReal q

Proof state:
a b : ℝ≥0
p q : ℝ
hpq : p.IsConjExponent q
⊢ a * b ≤ a ^ p / p.toNNReal + b ^ q / q.toNNReal

Tactic:
simpa [Real.coe_toNNReal, hpq.nonneg, hpq.symm.nonneg] using young_inequality a b hpq.toNNReal

Result:
no goals
-- Mathlib/Analysis/Normed/Order/UpperLower.lean
theorem IsUpperSet.cthickening' (hs : IsUpperSet s) (ε : ℝ) :
    IsUpperSet (cthickening ε s)

Proof state:
α : Type u_1
inst✝ : NormedOrderedGroup α
s : Set α
hs : IsUpperSet s
ε : ℝ
⊢ IsUpperSet (cthickening ε s)

Tactic:
rw [cthickening_eq_iInter_thickening'']

Result:
α : Type u_1
inst✝ : NormedOrderedGroup α
s : Set α
hs : IsUpperSet s
ε : ℝ
⊢ IsUpperSet (⋂ ε_1, ⋂ (_ : 0 ⊔ ε < ε_1), thickening ε_1 s)

Proof state:
α : Type u_1
inst✝ : NormedOrderedGroup α
s : Set α
hs : IsUpperSet s
ε : ℝ
⊢ IsUpperSet (⋂ ε_1, ⋂ (_ : 0 ⊔ ε < ε_1), thickening ε_1 s)

Tactic:
exact isUpperSet_iInter₂ fun δ _ => hs.thickening' _

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Cofinality.lean
theorem sum_lt_of_isRegular {ι : Type u} {f : ι → Cardinal} {c : Cardinal} (hc : IsRegular c)
    (hι : #ι < c) : (∀ i, f i < c) → sum f < c :=
  sum_lt_lift_of_isRegular.{u, u} hc (by rwa [lift_id])

Proof state:
ι : Type u
f : ι → Cardinal.{u}
c : Cardinal.{u}
hc : c.IsRegular
hι : #ι < c
⊢ lift.{u, u} #ι < c

Tactic:
rwa [lift_id]

Result:
no goals
-- Mathlib/Order/Filter/AtTopBot/Monoid.lean
theorem Tendsto.atTop_pow (hf : Tendsto f l atTop) {n : ℕ} (hn : 0 < n) :
    Tendsto (fun x => f x ^ n) l atTop

Proof state:
α : Type u_1
M : Type u_2
inst✝ : OrderedCommMonoid M
l : Filter α
f : α → M
hf : Tendsto f l atTop
n : ℕ
hn : 0 < n
x : α
hx : 1 ≤ f x
⊢ f x ≤ (fun x => f x ^ n) x

Tactic:
simpa only [pow_one] using pow_le_pow_right' hx hn

Result:
no goals

Proof state:
α : Type u_1
M : Type u_2
inst✝ : OrderedCommMonoid M
l : Filter α
f : α → M
hf : Tendsto f l atTop
n : ℕ
hn : 0 < n
⊢ Tendsto (fun x => f x ^ n) l atTop

Tactic:
refine tendsto_atTop_mono' _ ((hf.eventually_ge_atTop 1).mono fun x hx ↦ ?_) hf

Result:
α : Type u_1
M : Type u_2
inst✝ : OrderedCommMonoid M
l : Filter α
f : α → M
hf : Tendsto f l atTop
n : ℕ
hn : 0 < n
x : α
hx : 1 ≤ f x
⊢ f x ≤ (fun x => f x ^ n) x
-- Mathlib/Data/Matroid/Closure.lean
@[simp] lemma ground_subset_closure_iff : M.E ⊆ M.closure X ↔ M.closure X = M.E

Proof state:
α : Type u_2
M : Matroid α
X : Set α
⊢ M.E ⊆ M.closure X ↔ M.closure X = M.E

Tactic:
simp [M.closure_subset_ground X, subset_antisymm_iff]

Result:
no goals
-- Mathlib/AlgebraicGeometry/StructureSheaf.lean
theorem toStalk_comp_stalkToFiberRingHom (x : PrimeSpectrum.Top R) :
    toStalk R x ≫ stalkToFiberRingHom R x = CommRingCat.ofHom (algebraMap _ _)

Proof state:
R : Type u
inst✝ : CommRing R
x : ↑(PrimeSpectrum.Top R)
⊢ toStalk R x ≫ stalkToFiberRingHom R x = CommRingCat.ofHom (algebraMap R (Localization.AtPrime x.asIdeal))

Tactic:
rw [toStalk, Category.assoc, germ_comp_stalkToFiberRingHom]

Result:
R : Type u
inst✝ : CommRing R
x : ↑(PrimeSpectrum.Top R)
⊢ toOpen R ⊤ ≫ openToLocalization R ⊤ x True.intro = CommRingCat.ofHom (algebraMap R (Localization.AtPrime x.asIdeal))

Proof state:
R : Type u
inst✝ : CommRing R
x : ↑(PrimeSpectrum.Top R)
⊢ toOpen R ⊤ ≫ openToLocalization R ⊤ x True.intro = CommRingCat.ofHom (algebraMap R (Localization.AtPrime x.asIdeal))

Tactic:
rfl

Result:
no goals
-- Mathlib/Data/Fintype/Card.lean
theorem two_lt_card_iff : 2 < card α ↔ ∃ a b c : α, a ≠ b ∧ a ≠ c ∧ b ≠ c

Proof state:
α : Type u_1
inst✝ : Fintype α
⊢ 2 < card α ↔ ∃ a b c, a ≠ b ∧ a ≠ c ∧ b ≠ c

Tactic:
simp_rw [← Finset.card_univ, two_lt_card_iff, mem_univ, true_and]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/SchurComplement.lean
theorem det_fromBlocks₁₁ (A : Matrix m m α) (B : Matrix m n α) (C : Matrix n m α)
    (D : Matrix n n α) [Invertible A] :
    (Matrix.fromBlocks A B C D).det = det A * det (D - C * ⅟ A * B)

Proof state:
m : Type u_2
n : Type u_3
α : Type u_4
inst✝⁵ : Fintype m
inst✝⁴ : Fintype n
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : CommRing α
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
inst✝ : Invertible A
⊢ (fromBlocks A B C D).det = A.det * (D - C * ⅟A * B).det

Tactic:
rw [fromBlocks_eq_of_invertible₁₁ (A := A), det_mul, det_mul, det_fromBlocks_zero₂₁,
  det_fromBlocks_zero₂₁, det_fromBlocks_zero₁₂, det_one, det_one, one_mul, one_mul, mul_one]

Result:
no goals
-- Mathlib/Algebra/Order/Group/Pointwise/Interval.lean
theorem Iic_mul_Iic_subset' (a b : α) : Iic a * Iic b ⊆ Iic (a * b)

Proof state:
case intro.intro.intro.intro
α : Type u_1
inst✝³ : Mul α
inst✝² : Preorder α
inst✝¹ : MulLeftMono α
inst✝ : MulRightMono α
a b y : α
hya : y ∈ Iic a
z : α
hzb : z ∈ Iic b
⊢ (fun x1 x2 => x1 * x2) y z ∈ Iic (a * b)

Tactic:
exact mul_le_mul' hya hzb

Result:
no goals

Proof state:
α : Type u_1
inst✝³ : Mul α
inst✝² : Preorder α
inst✝¹ : MulLeftMono α
inst✝ : MulRightMono α
a b : α
⊢ Iic a * Iic b ⊆ Iic (a * b)

Tactic:
rintro x ⟨y, hya, z, hzb, rfl⟩

Result:
case intro.intro.intro.intro
α : Type u_1
inst✝³ : Mul α
inst✝² : Preorder α
inst✝¹ : MulLeftMono α
inst✝ : MulRightMono α
a b y : α
hya : y ∈ Iic a
z : α
hzb : z ∈ Iic b
⊢ (fun x1 x2 => x1 * x2) y z ∈ Iic (a * b)
-- Mathlib/Data/Matrix/Mul.lean
theorem mulVec_smul_assoc [Fintype n] (A : Matrix m n α) (b : n → α) (a : α) :
    A *ᵥ (a • b) = a • A *ᵥ b

Proof state:
case h
m : Type u_2
n : Type u_3
α : Type v
inst✝¹ : CommSemiring α
inst✝ : Fintype n
A : Matrix m n α
b : n → α
a : α
x✝ : m
⊢ (A *ᵥ a • b) x✝ = (a • A *ᵥ b) x✝

Tactic:
apply dotProduct_smul

Result:
no goals

Proof state:
m : Type u_2
n : Type u_3
α : Type v
inst✝¹ : CommSemiring α
inst✝ : Fintype n
A : Matrix m n α
b : n → α
a : α
⊢ A *ᵥ a • b = a • A *ᵥ b

Tactic:
ext

Result:
case h
m : Type u_2
n : Type u_3
α : Type v
inst✝¹ : CommSemiring α
inst✝ : Fintype n
A : Matrix m n α
b : n → α
a : α
x✝ : m
⊢ (A *ᵥ a • b) x✝ = (a • A *ᵥ b) x✝
-- Mathlib/MeasureTheory/Measure/ProbabilityMeasure.lean
theorem normalize_testAgainstNN (nonzero : μ ≠ 0) (f : Ω →ᵇ ℝ≥0) :
    μ.normalize.toFiniteMeasure.testAgainstNN f = μ.mass⁻¹ * μ.testAgainstNN f

Proof state:
Ω : Type u_1
inst✝¹ : Nonempty Ω
m0 : MeasurableSpace Ω
μ : FiniteMeasure Ω
inst✝ : TopologicalSpace Ω
nonzero : μ ≠ 0
f : Ω →ᵇ ℝ≥0
⊢ μ.normalize.toFiniteMeasure.testAgainstNN f = μ.mass⁻¹ * μ.testAgainstNN f

Tactic:
simp [μ.testAgainstNN_eq_mass_mul, inv_mul_cancel_left₀ <| μ.mass_nonzero_iff.mpr nonzero]

Result:
no goals
-- Mathlib/Data/List/Iterate.lean
theorem length_iterate (f : α → α) (a : α) (n : ℕ) : length (iterate f a n) = n

Proof state:
α : Type u_1
f : α → α
a : α
n : ℕ
⊢ (iterate f a n).length = n

Tactic:
induction n generalizing a <;> simp [*]

Result:
no goals
-- Mathlib/Algebra/ContinuedFractions/Translations.lean
theorem partDen_none_iff_s_none : g.partDens.get? n = none ↔ g.s.get? n = none

Proof state:
α : Type u_1
g : GenContFract α
n : ℕ
⊢ g.partDens.get? n = none ↔ g.s.get? n = none

Tactic:
cases s_nth_eq : g.s.get? n <;> simp [partDens, s_nth_eq]

Result:
no goals