harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/Convex/Basic.lean
theorem convex_iff_pointwise_add_subset :
    Convex 𝕜 s ↔ ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → a • s + b • s ⊆ s :=
  Iff.intro
    (by
      rintro hA a b ha hb hab w ⟨au, ⟨u, hu, rfl⟩, bv, ⟨v, hv, rfl⟩, rfl⟩
      exact hA hu hv ha hb hab)
    fun h _ hx _ hy _ _ ha hb hab => (h ha hb hab) (Set.add_mem_add ⟨_, hx, rfl⟩ ⟨_, hy, rfl⟩)

Proof state:
case intro.intro.intro.intro.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : SMul 𝕜 E
s : Set E
hA : Convex 𝕜 s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
u : E
hu : u ∈ s
v : E
hv : v ∈ s
⊢ (fun x1 x2 => x1 + x2) ((fun x => a • x) u) ((fun x => b • x) v) ∈ s

Tactic:
exact hA hu hv ha hb hab

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : SMul 𝕜 E
s : Set E
⊢ Convex 𝕜 s → ∀ ⦃a b : 𝕜⦄, 0 ≤ a → 0 ≤ b → a + b = 1 → a • s + b • s ⊆ s

Tactic:
rintro hA a b ha hb hab w ⟨au, ⟨u, hu, rfl⟩, bv, ⟨v, hv, rfl⟩, rfl⟩

Result:
case intro.intro.intro.intro.intro.intro.intro.intro
𝕜 : Type u_1
E : Type u_2
inst✝² : OrderedSemiring 𝕜
inst✝¹ : AddCommMonoid E
inst✝ : SMul 𝕜 E
s : Set E
hA : Convex 𝕜 s
a b : 𝕜
ha : 0 ≤ a
hb : 0 ≤ b
hab : a + b = 1
u : E
hu : u ∈ s
v : E
hv : v ∈ s
⊢ (fun x1 x2 => x1 + x2) ((fun x => a • x) u) ((fun x => b • x) v) ∈ s
-- Mathlib/Analysis/RCLike/Basic.lean
lemma nonpos_iff_exists_ofReal : z ≤ 0 ↔ ∃ x ≤ (0 : ℝ), x = z

Proof state:
K : Type u_1
inst✝ : RCLike K
z : K
⊢ z ≤ 0 ↔ ∃ x ≤ 0, ↑x = z

Tactic:
simp_rw [nonpos_iff (K := K), ext_iff (K := K)]

Result:
K : Type u_1
inst✝ : RCLike K
z : K
⊢ re z ≤ 0 ∧ im z = 0 ↔ ∃ x ≤ 0, re ↑x = re z ∧ im ↑x = im z

Proof state:
K : Type u_1
inst✝ : RCLike K
z : K
⊢ re z ≤ 0 ∧ im z = 0 ↔ ∃ x ≤ 0, re ↑x = re z ∧ im ↑x = im z

Tactic:
aesop

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Option/Lemmas.lean
theorem filter_eq_none {p : α → Bool} :
    o.filter p = none ↔ o = none ∨ ∀ a, a ∈ o → ¬ p a

Proof state:
α : Type u_1
o : Option α
p : α → Bool
⊢ Option.filter p o = none ↔ o = none ∨ ∀ (a : α), a ∈ o → ¬p a = true

Tactic:
cases o <;> simp [filter_some]

Result:
no goals
-- Mathlib/MeasureTheory/Function/LpSpace/Basic.lean
theorem norm_indicatorConstLp (hp_ne_zero : p ≠ 0) (hp_ne_top : p ≠ ∞) :
    ‖indicatorConstLp p hs hμs c‖ = ‖c‖ * (μ s).toReal ^ (1 / p.toReal)

Proof state:
α : Type u_1
E : Type u_4
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝ : NormedAddCommGroup E
s : Set α
hs : MeasurableSet s
hμs : μ s ≠ ⊤
c : E
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
⊢ ‖indicatorConstLp p hs hμs c‖ = ‖c‖ * (μ s).toReal ^ (1 / p.toReal)

Tactic:
rw [Lp.norm_def, eLpNorm_congr_ae indicatorConstLp_coeFn,
  eLpNorm_indicator_const hs hp_ne_zero hp_ne_top, ENNReal.toReal_mul, ENNReal.toReal_rpow,
  toReal_enorm]

Result:
no goals
-- Mathlib/AlgebraicTopology/DoldKan/Faces.lean
theorem of_comp {Y Z : C} {q n : ℕ} {φ : Y ⟶ X _⦋n + 1⦌} (v : HigherFacesVanish q φ) (f : Z ⟶ Y) :
    HigherFacesVanish q (f ≫ φ) := fun j hj => by rw [assoc, v j hj, comp_zero]

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
X : SimplicialObject C
Y Z : C
q n : ℕ
φ : Y ⟶ X _⦋n + 1⦌
v : HigherFacesVanish q φ
f : Z ⟶ Y
j : Fin (n + 1)
hj : n + 1 ≤ ↑j + q
⊢ (f ≫ φ) ≫ X.δ j.succ = 0

Tactic:
rw [assoc, v j hj, comp_zero]

Result:
no goals
-- Mathlib/Data/Finset/Dedup.lean
theorem toFinset_ssubset : s.toFinset ⊂ t.toFinset ↔ s ⊂ t

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
⊢ s.toFinset ⊂ t.toFinset ↔ s ⊂ t

Tactic:
simp_rw [Finset.ssubset_def, toFinset_subset]

Result:
α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
⊢ s ⊆ t ∧ ¬t ⊆ s ↔ s ⊂ t

Proof state:
α : Type u_1
inst✝ : DecidableEq α
s t : Multiset α
⊢ s ⊆ t ∧ ¬t ⊆ s ↔ s ⊂ t

Tactic:
rfl

Result:
no goals
-- Mathlib/Algebra/Module/Submodule/LinearMap.lean
lemma restrict_sub {R M M₁ : Type*}
    [Ring R] [AddCommGroup M] [AddCommGroup M₁] [Module R M] [Module R M₁]
    {p : Submodule R M} {q : Submodule R M₁} {f g : M →ₗ[R] M₁}
    (hf : MapsTo f p q) (hg : MapsTo g p q)
    (hfg : MapsTo (f - g) p q := fun _ hx ↦ q.sub_mem (hf hx) (hg hx)) :
    f.restrict hf - g.restrict hg = (f - g).restrict hfg

Proof state:
case h.a
R : Type u_10
M : Type u_11
M₁ : Type u_12
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup M₁
inst✝¹ : Module R M
inst✝ : Module R M₁
p : Submodule R M
q : Submodule R M₁
f g : M →ₗ[R] M₁
hf : MapsTo ⇑f ↑p ↑q
hg : MapsTo ⇑g ↑p ↑q
hfg : optParam (MapsTo ⇑(f - g) ↑p ↑q) ⋯
x✝ : ↥p
⊢ ↑((f.restrict hf - g.restrict hg) x✝) = ↑(((f - g).restrict hfg) x✝)

Tactic:
simp

Result:
no goals

Proof state:
R : Type u_10
M : Type u_11
M₁ : Type u_12
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup M₁
inst✝¹ : Module R M
inst✝ : Module R M₁
p : Submodule R M
q : Submodule R M₁
f g : M →ₗ[R] M₁
hf : MapsTo ⇑f ↑p ↑q
hg : MapsTo ⇑g ↑p ↑q
hfg : optParam (MapsTo ⇑(f - g) ↑p ↑q) ⋯
⊢ f.restrict hf - g.restrict hg = (f - g).restrict hfg

Tactic:
ext

Result:
case h.a
R : Type u_10
M : Type u_11
M₁ : Type u_12
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup M₁
inst✝¹ : Module R M
inst✝ : Module R M₁
p : Submodule R M
q : Submodule R M₁
f g : M →ₗ[R] M₁
hf : MapsTo ⇑f ↑p ↑q
hg : MapsTo ⇑g ↑p ↑q
hfg : optParam (MapsTo ⇑(f - g) ↑p ↑q) ⋯
x✝ : ↥p
⊢ ↑((f.restrict hf - g.restrict hg) x✝) = ↑(((f - g).restrict hfg) x✝)
-- Mathlib/GroupTheory/Submonoid/Inverses.lean
theorem mul_leftInvEquiv (x : S.leftInv) : (x : M) * S.leftInvEquiv hS x = 1

Proof state:
M : Type u_1
inst✝ : CommMonoid M
S : Submonoid M
hS : S ≤ IsUnit.submonoid M
x : ↥S.leftInv
⊢ ↑x * ↑((S.leftInvEquiv hS) x) = 1

Tactic:
simp only [leftInvEquiv_apply, fromCommLeftInv, mul_fromLeftInv]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Diam.lean
@[simp]
lemma diam_eq_zero : G.diam = 0 ↔ G.ediam = ⊤ ∨ Subsingleton α

Proof state:
α : Type u_1
G : SimpleGraph α
⊢ G.diam = 0 ↔ G.ediam = ⊤ ∨ Subsingleton α

Tactic:
rw [diam, ENat.toNat_eq_zero, or_comm, ediam_eq_zero_iff_subsingleton]

Result:
no goals
-- Mathlib/Algebra/Lie/Weights/Cartan.lean
theorem le_zeroRootSubalgebra : H ≤ zeroRootSubalgebra R L H

Proof state:
R : Type u_1
L : Type u_2
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
H : LieSubalgebra R L
inst✝ : LieRing.IsNilpotent ↥H
⊢ H.toLieSubmodule ≤ rootSpace H 0

Tactic:
exact toLieSubmodule_le_rootSpace_zero R L H

Result:
no goals

Proof state:
R : Type u_1
L : Type u_2
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
H : LieSubalgebra R L
inst✝ : LieRing.IsNilpotent ↥H
⊢ H ≤ zeroRootSubalgebra R L H

Tactic:
rw [← LieSubalgebra.toSubmodule_le_toSubmodule, ← H.coe_toLieSubmodule,
  coe_zeroRootSubalgebra, LieSubmodule.toSubmodule_le_toSubmodule]

Result:
R : Type u_1
L : Type u_2
inst✝³ : CommRing R
inst✝² : LieRing L
inst✝¹ : LieAlgebra R L
H : LieSubalgebra R L
inst✝ : LieRing.IsNilpotent ↥H
⊢ H.toLieSubmodule ≤ rootSpace H 0
-- Mathlib/CategoryTheory/Monoidal/Cartesian/Comon_.lean
theorem counit_eq_from (A : Comon_ C) : A.counit = terminal.from A.X

Proof state:
C : Type u
inst✝² : Category.{v, u} C
inst✝¹ : HasTerminal C
inst✝ : HasBinaryProducts C
A : Comon_ C
⊢ A.counit = terminal.from A.X

Tactic:
ext

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/LaxMilgram.lean
theorem isClosed_range (coercive : IsCoercive B) : IsClosed (range B♯ : Set V)

Proof state:
case intro.intro
V : Type u
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : CompleteSpace V
B : V →L[ℝ] V →L[ℝ] ℝ
coercive : IsCoercive B
w✝ : ℝ≥0
left✝ : 0 < w✝
antilipschitz : AntilipschitzWith w✝ ⇑(continuousLinearMapOfBilin B)
⊢ IsClosed ↑(range (continuousLinearMapOfBilin B))

Tactic:
exact antilipschitz.isClosed_range B♯.uniformContinuous

Result:
no goals

Proof state:
V : Type u
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : CompleteSpace V
B : V →L[ℝ] V →L[ℝ] ℝ
coercive : IsCoercive B
⊢ IsClosed ↑(range (continuousLinearMapOfBilin B))

Tactic:
rcases coercive.antilipschitz with ⟨_, _, antilipschitz⟩

Result:
case intro.intro
V : Type u
inst✝² : NormedAddCommGroup V
inst✝¹ : InnerProductSpace ℝ V
inst✝ : CompleteSpace V
B : V →L[ℝ] V →L[ℝ] ℝ
coercive : IsCoercive B
w✝ : ℝ≥0
left✝ : 0 < w✝
antilipschitz : AntilipschitzWith w✝ ⇑(continuousLinearMapOfBilin B)
⊢ IsClosed ↑(range (continuousLinearMapOfBilin B))
-- Mathlib/RingTheory/Nilpotent/Lemmas.lean
theorem RingHom.ker_isRadical_iff_reduced_of_surjective {S F} [CommSemiring R] [CommRing S]
    [FunLike F R S] [RingHomClass F R S] {f : F} (hf : Function.Surjective f) :
    (RingHom.ker f).IsRadical ↔ IsReduced S

Proof state:
R : Type u_1
S : Type u_3
F : Type u_4
inst✝³ : CommSemiring R
inst✝² : CommRing S
inst✝¹ : FunLike F R S
inst✝ : RingHomClass F R S
f : F
hf : Surjective ⇑f
⊢ (ker f).IsRadical ↔ IsReduced S

Tactic:
simp_rw [isReduced_iff, hf.forall, IsNilpotent, ← map_pow, ← RingHom.mem_ker]

Result:
R : Type u_1
S : Type u_3
F : Type u_4
inst✝³ : CommSemiring R
inst✝² : CommRing S
inst✝¹ : FunLike F R S
inst✝ : RingHomClass F R S
f : F
hf : Surjective ⇑f
⊢ (ker f).IsRadical ↔ ∀ (x : R), (∃ n, x ^ n ∈ ker f) → x ∈ ker f

Proof state:
R : Type u_1
S : Type u_3
F : Type u_4
inst✝³ : CommSemiring R
inst✝² : CommRing S
inst✝¹ : FunLike F R S
inst✝ : RingHomClass F R S
f : F
hf : Surjective ⇑f
⊢ (ker f).IsRadical ↔ ∀ (x : R), (∃ n, x ^ n ∈ ker f) → x ∈ ker f

Tactic:
rfl

Result:
no goals
-- Mathlib/Algebra/Homology/ShortComplex/SnakeLemma.lean
@[reassoc (attr := simp)] lemma L₁_f_φ₁ : S.L₀'.f ≫ S.φ₁ = S.v₁₂.τ₁

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Abelian C
S : SnakeInput C
⊢ S.L₀'.f ≫ S.φ₁ = S.v₁₂.τ₁

Tactic:
dsimp only [L₀']

Result:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Abelian C
S : SnakeInput C
⊢ pullback.lift S.L₁.f 0 ⋯ ≫ S.φ₁ = S.v₁₂.τ₁

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Abelian C
S : SnakeInput C
⊢ pullback.lift S.L₁.f 0 ⋯ ≫ S.φ₁ = S.v₁₂.τ₁

Tactic:
simp only [← cancel_mono S.L₂.f, assoc, φ₁_L₂_f, φ₂, pullback.lift_fst_assoc,
  S.v₁₂.comm₁₂]

Result:
no goals
-- Mathlib/CategoryTheory/Functor/KanExtension/Adjunction.lean
@[simp]
lemma lanAdjunction_unit : (L.lanAdjunction H).unit = L.lanUnit

Proof state:
case w.h
C : Type u_1
D : Type u_2
inst✝³ : Category.{u_4, u_1} C
inst✝² : Category.{u_6, u_2} D
L : C ⥤ D
H : Type u_3
inst✝¹ : Category.{u_5, u_3} H
inst✝ : ∀ (F : C ⥤ H), L.HasLeftKanExtension F
F : C ⥤ H
⊢ L.lanUnit.app F ≫ 𝟙 (L ⋙ L.lan.obj F) = L.lanUnit.app F

Tactic:
simp

Result:
no goals

Proof state:
case w.h
C : Type u_1
D : Type u_2
inst✝³ : Category.{u_4, u_1} C
inst✝² : Category.{u_6, u_2} D
L : C ⥤ D
H : Type u_3
inst✝¹ : Category.{u_5, u_3} H
inst✝ : ∀ (F : C ⥤ H), L.HasLeftKanExtension F
F : C ⥤ H
⊢ (L.lanAdjunction H).unit.app F = L.lanUnit.app F

Tactic:
dsimp [lanAdjunction, homEquivOfIsLeftKanExtension]

Result:
case w.h
C : Type u_1
D : Type u_2
inst✝³ : Category.{u_4, u_1} C
inst✝² : Category.{u_6, u_2} D
L : C ⥤ D
H : Type u_3
inst✝¹ : Category.{u_5, u_3} H
inst✝ : ∀ (F : C ⥤ H), L.HasLeftKanExtension F
F : C ⥤ H
⊢ L.lanUnit.app F ≫ 𝟙 (L ⋙ L.lan.obj F) = L.lanUnit.app F

Proof state:
C : Type u_1
D : Type u_2
inst✝³ : Category.{u_4, u_1} C
inst✝² : Category.{u_6, u_2} D
L : C ⥤ D
H : Type u_3
inst✝¹ : Category.{u_5, u_3} H
inst✝ : ∀ (F : C ⥤ H), L.HasLeftKanExtension F
⊢ (L.lanAdjunction H).unit = L.lanUnit

Tactic:
ext F : 2

Result:
case w.h
C : Type u_1
D : Type u_2
inst✝³ : Category.{u_4, u_1} C
inst✝² : Category.{u_6, u_2} D
L : C ⥤ D
H : Type u_3
inst✝¹ : Category.{u_5, u_3} H
inst✝ : ∀ (F : C ⥤ H), L.HasLeftKanExtension F
F : C ⥤ H
⊢ (L.lanAdjunction H).unit.app F = L.lanUnit.app F
-- Mathlib/Combinatorics/Enumerative/IncidenceAlgebra.lean
lemma zeta_mul_mu [DecidableRel (α := α) (· ≤ ·)] : (zeta 𝕜 * mu 𝕜 : IncidenceAlgebra 𝕜 α) = 1

Proof state:
𝕜 : Type u_2
α : Type u_5
inst✝⁴ : Ring 𝕜
inst✝³ : PartialOrder α
inst✝² : LocallyFiniteOrder α
inst✝¹ : DecidableEq α
inst✝ : DecidableRel fun x1 x2 => x1 ≤ x2
⊢ zeta 𝕜 * mu 𝕜 = 1

Tactic:
rw [mu_eq_mu', zeta_mul_mu']

Result:
no goals
-- Mathlib/Order/Interval/Set/UnorderedInterval.lean
@[simp] lemma uIoo_of_le (h : a ≤ b) : uIoo a b = Ioo a b

Proof state:
α : Type u_1
inst✝ : LinearOrder α
a b : α
h : a ≤ b
⊢ uIoo a b = Ioo a b

Tactic:
rw [uIoo, inf_eq_left.2 h, sup_eq_right.2 h]

Result:
no goals
-- Mathlib/Topology/CompactOpen.lean
lemma nhds_compactOpen (f : C(X, Y)) :
    𝓝 f = ⨅ (K : Set X) (_ : IsCompact K) (U : Set Y) (_ : IsOpen U) (_ : MapsTo f K U),
      𝓟 {g : C(X, Y) | MapsTo g K U}

Proof state:
X : Type u_2
Y : Type u_3
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : C(X, Y)
⊢ 𝓝 f = ⨅ K, ⨅ (_ : IsCompact K), ⨅ U, ⨅ (_ : IsOpen U), ⨅ (_ : MapsTo (⇑f) K U), 𝓟 {g | MapsTo (⇑g) K U}

Tactic:
simp_rw [compactOpen_eq, nhds_generateFrom, mem_setOf_eq, @and_comm (f ∈ _), iInf_and,
  ← image_prod, iInf_image, biInf_prod, mem_setOf_eq]

Result:
no goals
-- Mathlib/Topology/Semicontinuous.lean
theorem LowerSemicontinuousAt.add' {f g : α → γ} (hf : LowerSemicontinuousAt f x)
    (hg : LowerSemicontinuousAt g x)
    (hcont : ContinuousAt (fun p : γ × γ => p.1 + p.2) (f x, g x)) :
    LowerSemicontinuousAt (fun z => f z + g z) x

Proof state:
α : Type u_1
inst✝³ : TopologicalSpace α
x : α
γ : Type u_4
inst✝² : LinearOrderedAddCommMonoid γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f g : α → γ
hcont : ContinuousAt (fun p => p.1 + p.2) (f x, g x)
hf : LowerSemicontinuousWithinAt f univ x
hg : LowerSemicontinuousWithinAt g univ x
⊢ LowerSemicontinuousWithinAt (fun z => f z + g z) univ x

Tactic:
exact hf.add' hg hcont

Result:
no goals

Proof state:
α : Type u_1
inst✝³ : TopologicalSpace α
x : α
γ : Type u_4
inst✝² : LinearOrderedAddCommMonoid γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f g : α → γ
hf : LowerSemicontinuousAt f x
hg : LowerSemicontinuousAt g x
hcont : ContinuousAt (fun p => p.1 + p.2) (f x, g x)
⊢ LowerSemicontinuousAt (fun z => f z + g z) x

Tactic:
simp_rw [← lowerSemicontinuousWithinAt_univ_iff] at *

Result:
α : Type u_1
inst✝³ : TopologicalSpace α
x : α
γ : Type u_4
inst✝² : LinearOrderedAddCommMonoid γ
inst✝¹ : TopologicalSpace γ
inst✝ : OrderTopology γ
f g : α → γ
hcont : ContinuousAt (fun p => p.1 + p.2) (f x, g x)
hf : LowerSemicontinuousWithinAt f univ x
hg : LowerSemicontinuousWithinAt g univ x
⊢ LowerSemicontinuousWithinAt (fun z => f z + g z) univ x
-- Mathlib/Data/Nat/ModEq.lean
theorem modEq_and_modEq_iff_modEq_mul {a b m n : ℕ} (hmn : m.Coprime n) :
    a ≡ b [MOD m] ∧ a ≡ b [MOD n] ↔ a ≡ b [MOD m * n] :=
  ⟨fun h => by
    rw [Nat.modEq_iff_dvd, Nat.modEq_iff_dvd, ← Int.dvd_natAbs, Int.natCast_dvd_natCast,
      ← Int.dvd_natAbs, Int.natCast_dvd_natCast] at h
    rw [Nat.modEq_iff_dvd, ← Int.dvd_natAbs, Int.natCast_dvd_natCast]
    exact hmn.mul_dvd_of_dvd_of_dvd h.1 h.2,
   fun h => ⟨h.of_mul_right _, h.of_mul_left _⟩⟩

Proof state:
a b m n : ℕ
hmn : m.Coprime n
h : m ∣ (↑b - ↑a).natAbs ∧ n ∣ (↑b - ↑a).natAbs
⊢ a ≡ b [MOD m * n]

Tactic:
rw [Nat.modEq_iff_dvd, ← Int.dvd_natAbs, Int.natCast_dvd_natCast]

Result:
a b m n : ℕ
hmn : m.Coprime n
h : m ∣ (↑b - ↑a).natAbs ∧ n ∣ (↑b - ↑a).natAbs
⊢ m * n ∣ (↑b - ↑a).natAbs

Proof state:
a b m n : ℕ
hmn : m.Coprime n
h : a ≡ b [MOD m] ∧ a ≡ b [MOD n]
⊢ a ≡ b [MOD m * n]

Tactic:
rw [Nat.modEq_iff_dvd, Nat.modEq_iff_dvd, ← Int.dvd_natAbs, Int.natCast_dvd_natCast,
  ← Int.dvd_natAbs, Int.natCast_dvd_natCast] at h

Result:
a b m n : ℕ
hmn : m.Coprime n
h : m ∣ (↑b - ↑a).natAbs ∧ n ∣ (↑b - ↑a).natAbs
⊢ a ≡ b [MOD m * n]

Proof state:
a b m n : ℕ
hmn : m.Coprime n
h : m ∣ (↑b - ↑a).natAbs ∧ n ∣ (↑b - ↑a).natAbs
⊢ m * n ∣ (↑b - ↑a).natAbs

Tactic:
exact hmn.mul_dvd_of_dvd_of_dvd h.1 h.2

Result:
no goals
-- Mathlib/NumberTheory/ModularForms/SlashActions.lean
theorem SlashAction.smul_slash_of_tower {R β G α : Type*} (γ : Type*) [Group G] [AddGroup α]
    [Monoid γ] [MulAction γ α] [SMul R γ] [SMul R α] [IsScalarTower R γ α] [SlashAction β G α γ]
    (k : β) (g : G) (a : α) (r : R) : (r • a) ∣[k;γ] g = r • a ∣[k;γ] g

Proof state:
R : Type u_1
β : Type u_2
G : Type u_3
α : Type u_4
γ : Type u_5
inst✝⁷ : Group G
inst✝⁶ : AddGroup α
inst✝⁵ : Monoid γ
inst✝⁴ : MulAction γ α
inst✝³ : SMul R γ
inst✝² : SMul R α
inst✝¹ : IsScalarTower R γ α
inst✝ : SlashAction β G α γ
k : β
g : G
a : α
r : R
⊢ (r • a) ∣[k;γ] g = r • a ∣[k;γ] g

Tactic:
rw [← smul_one_smul γ r a, SlashAction.smul_slash, smul_one_smul]

Result:
no goals
-- Mathlib/SetTheory/Ordinal/Arithmetic.lean
theorem add_eq_zero_iff {a b : Ordinal} : a + b = 0 ↔ a = 0 ∧ b = 0 :=
  inductionOn₂ a b fun α r _ β s _ => by
    simp_rw [← type_sum_lex, type_eq_zero_iff_isEmpty]
    exact isEmpty_sum

Proof state:
a b : Ordinal.{u_4}
α : Type u_4
r : α → α → Prop
x✝¹ : IsWellOrder α r
β : Type u_4
s : β → β → Prop
x✝ : IsWellOrder β s
⊢ type r + type s = 0 ↔ type r = 0 ∧ type s = 0

Tactic:
simp_rw [← type_sum_lex, type_eq_zero_iff_isEmpty]

Result:
a b : Ordinal.{u_4}
α : Type u_4
r : α → α → Prop
x✝¹ : IsWellOrder α r
β : Type u_4
s : β → β → Prop
x✝ : IsWellOrder β s
⊢ IsEmpty (α ⊕ β) ↔ IsEmpty α ∧ IsEmpty β

Proof state:
a b : Ordinal.{u_4}
α : Type u_4
r : α → α → Prop
x✝¹ : IsWellOrder α r
β : Type u_4
s : β → β → Prop
x✝ : IsWellOrder β s
⊢ IsEmpty (α ⊕ β) ↔ IsEmpty α ∧ IsEmpty β

Tactic:
exact isEmpty_sum

Result:
no goals
-- Mathlib/AlgebraicGeometry/ValuativeCriterion.lean
lemma ValuativeCriterion.iff {f : X ⟶ Y} :
    ValuativeCriterion f ↔ Existence f ∧ Uniqueness f

Proof state:
X Y : Scheme
f : X ⟶ Y
⊢ (∀ (x : ValuativeCommSq f), Nonempty (Unique ⋯.LiftStruct)) ↔
    (∀ (x : ValuativeCommSq f), ⋯.HasLift) ∧ ∀ (x : ValuativeCommSq f), Subsingleton ⋯.LiftStruct

Tactic:
simp_rw [← forall_and, unique_iff_subsingleton_and_nonempty, and_comm, CommSq.HasLift.iff]

Result:
no goals

Proof state:
X Y : Scheme
f : X ⟶ Y
⊢ ValuativeCriterion f ↔ Existence f ∧ Uniqueness f

Tactic:
show (∀ _, _) ↔ (∀ _, _) ∧ (∀ _, _)

Result:
X Y : Scheme
f : X ⟶ Y
⊢ (∀ (x : ValuativeCommSq f), Nonempty (Unique ⋯.LiftStruct)) ↔
    (∀ (x : ValuativeCommSq f), ⋯.HasLift) ∧ ∀ (x : ValuativeCommSq f), Subsingleton ⋯.LiftStruct
-- Mathlib/Analysis/Calculus/Deriv/Comp.lean
theorem HasDerivAtFilter.scomp (hg : HasDerivAtFilter g₁ g₁' (h x) L')
    (hh : HasDerivAtFilter h h' x L) (hL : Tendsto h L L') :
    HasDerivAtFilter (g₁ ∘ h) (h' • g₁') x L

Proof state:
𝕜 : Type u
inst✝⁶ : NontriviallyNormedField 𝕜
F : Type v
inst✝⁵ : NormedAddCommGroup F
inst✝⁴ : NormedSpace 𝕜 F
x : 𝕜
L : Filter 𝕜
𝕜' : Type u_1
inst✝³ : NontriviallyNormedField 𝕜'
inst✝² : NormedAlgebra 𝕜 𝕜'
inst✝¹ : NormedSpace 𝕜' F
inst✝ : IsScalarTower 𝕜 𝕜' F
h : 𝕜 → 𝕜'
h' : 𝕜'
g₁ : 𝕜' → F
g₁' : F
L' : Filter 𝕜'
hg : HasDerivAtFilter g₁ g₁' (h x) L'
hh : HasDerivAtFilter h h' x L
hL : Tendsto h L L'
⊢ HasDerivAtFilter (g₁ ∘ h) (h' • g₁') x L

Tactic:
simpa using ((hg.restrictScalars 𝕜).comp x hh hL).hasDerivAtFilter

Result:
no goals
-- Mathlib/Topology/CompactOpen.lean
theorem continuous_curry [LocallyCompactSpace (X × Y)] :
    Continuous (curry : C(X × Y, Z) → C(X, C(Y, Z)))

Proof state:
case h
X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : LocallyCompactSpace (X × Y)
⊢ Continuous (Function.uncurry fun x y => x.curry y)

Tactic:
apply continuous_of_continuous_uncurry

Result:
case h.h
X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : LocallyCompactSpace (X × Y)
⊢ Continuous (Function.uncurry fun x y => (Function.uncurry (fun x y => x.curry y) x) y)

Proof state:
case h.h
X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : LocallyCompactSpace (X × Y)
⊢ Continuous (Function.uncurry fun x y => (Function.uncurry (fun x y => x.curry y) x) y)

Tactic:
rw [← (Homeomorph.prodAssoc _ _ _).symm.comp_continuous_iff']

Result:
case h.h
X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : LocallyCompactSpace (X × Y)
⊢ Continuous
    ((Function.uncurry fun x y => (Function.uncurry (fun x y => x.curry y) x) y) ∘
      ⇑(Homeomorph.prodAssoc C(X × Y, Z) X Y).symm)

Proof state:
X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : LocallyCompactSpace (X × Y)
⊢ Continuous curry

Tactic:
apply continuous_of_continuous_uncurry

Result:
case h
X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : LocallyCompactSpace (X × Y)
⊢ Continuous (Function.uncurry fun x y => x.curry y)

Proof state:
case h.h
X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝³ : TopologicalSpace X
inst✝² : TopologicalSpace Y
inst✝¹ : TopologicalSpace Z
inst✝ : LocallyCompactSpace (X × Y)
⊢ Continuous
    ((Function.uncurry fun x y => (Function.uncurry (fun x y => x.curry y) x) y) ∘
      ⇑(Homeomorph.prodAssoc C(X × Y, Z) X Y).symm)

Tactic:
exact continuous_eval

Result:
no goals
-- Mathlib/MeasureTheory/Integral/IntegrableOn.lean
theorem IntegrableOn.restrict (h : IntegrableOn f s μ) (hs : MeasurableSet s) :
    IntegrableOn f s (μ.restrict t)

Proof state:
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f : α → E
s t : Set α
μ : Measure α
h : IntegrableOn f s μ
hs : MeasurableSet s
⊢ IntegrableOn f s (μ.restrict t)

Tactic:
rw [IntegrableOn, Measure.restrict_restrict hs]

Result:
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f : α → E
s t : Set α
μ : Measure α
h : IntegrableOn f s μ
hs : MeasurableSet s
⊢ Integrable f (μ.restrict (s ∩ t))

Proof state:
α : Type u_1
E : Type u_4
inst✝¹ : MeasurableSpace α
inst✝ : NormedAddCommGroup E
f : α → E
s t : Set α
μ : Measure α
h : IntegrableOn f s μ
hs : MeasurableSet s
⊢ Integrable f (μ.restrict (s ∩ t))

Tactic:
exact h.mono_set inter_subset_left

Result:
no goals
-- Mathlib/RingTheory/Smooth/Kaehler.lean
theorem Algebra.FormallySmooth.iff_injective_and_projective :
    Algebra.FormallySmooth R S ↔
        Function.Injective (kerCotangentToTensor R P S) ∧ Module.Projective S (Ω[S⁄R])

Proof state:
case hs
R P S : Type u
inst✝⁷ : CommRing R
inst✝⁶ : CommRing P
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R P
inst✝³ : Algebra P S
inst✝² : Algebra R S
inst✝¹ : IsScalarTower R P S
hf : Surjective ⇑(algebraMap P S)
inst✝ : FormallySmooth R P
⊢ Surjective ⇑(mapBaseChange R P S)

Tactic:
exact KaehlerDifferential.mapBaseChange_surjective _ _ _ hf

Result:
no goals

Proof state:
R P S : Type u
inst✝⁷ : CommRing R
inst✝⁶ : CommRing P
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R P
inst✝³ : Algebra P S
inst✝² : Algebra R S
inst✝¹ : IsScalarTower R P S
hf : Surjective ⇑(algebraMap P S)
inst✝ : FormallySmooth R P
⊢ FormallySmooth R S ↔ Function.Injective ⇑(kerCotangentToTensor R P S) ∧ Module.Projective S (Ω[S⁄R])

Tactic:
rw [Algebra.FormallySmooth.iff_injective_and_split hf,
  ← Module.Projective.iff_split_of_projective]

Result:
case hs
R P S : Type u
inst✝⁷ : CommRing R
inst✝⁶ : CommRing P
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R P
inst✝³ : Algebra P S
inst✝² : Algebra R S
inst✝¹ : IsScalarTower R P S
hf : Surjective ⇑(algebraMap P S)
inst✝ : FormallySmooth R P
⊢ Surjective ⇑(mapBaseChange R P S)