harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/List/Sort.lean
theorem erase_orderedInsert [DecidableEq α] [IsRefl α r] (x : α) (xs : List α) :
    (xs.orderedInsert r x).erase x = xs

Proof state:
case h
α : Type u
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : DecidableEq α
inst✝ : IsRefl α r
x : α
xs : List α
h : x ∈ takeWhile (fun b => decide ¬r x b) xs
⊢ False

Tactic:
replace h := mem_takeWhile_imp h

Result:
case h
α : Type u
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : DecidableEq α
inst✝ : IsRefl α r
x : α
xs : List α
h : (decide ¬r x x) = true
⊢ False

Proof state:
case h
α : Type u
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : DecidableEq α
inst✝ : IsRefl α r
x : α
xs : List α
h : (decide ¬r x x) = true
⊢ False

Tactic:
simp [refl x] at h

Result:
no goals

Proof state:
α : Type u
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : DecidableEq α
inst✝ : IsRefl α r
x : α
xs : List α
⊢ (orderedInsert r x xs).erase x = xs

Tactic:
rw [orderedInsert_eq_take_drop, erase_append_right, List.erase_cons_head,
  takeWhile_append_dropWhile]

Result:
case h
α : Type u
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : DecidableEq α
inst✝ : IsRefl α r
x : α
xs : List α
⊢ x ∉ takeWhile (fun b => decide ¬r x b) xs

Proof state:
case h
α : Type u
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : DecidableEq α
inst✝ : IsRefl α r
x : α
xs : List α
⊢ x ∉ takeWhile (fun b => decide ¬r x b) xs

Tactic:
intro h

Result:
case h
α : Type u
r : α → α → Prop
inst✝² : DecidableRel r
inst✝¹ : DecidableEq α
inst✝ : IsRefl α r
x : α
xs : List α
h : x ∈ takeWhile (fun b => decide ¬r x b) xs
⊢ False
-- Mathlib/Algebra/Homology/ShortComplex/LeftHomology.lean
@[simp] lemma ofIsColimitCokernelCofork_f' (hg : S.g = 0) (c : CokernelCofork S.f)
    (hc : IsColimit c) : (ofIsColimitCokernelCofork S hg c hc).f' = S.f

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
S : ShortComplex C
hg : S.g = 0
c : CokernelCofork S.f
hc : IsColimit c
⊢ S.f = S.f ≫ 𝟙 S.X₂

Tactic:
rw [comp_id]

Result:
no goals

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
S : ShortComplex C
hg : S.g = 0
c : CokernelCofork S.f
hc : IsColimit c
⊢ (ofIsColimitCokernelCofork S hg c hc).f' = S.f

Tactic:
rw [← cancel_mono (ofIsColimitCokernelCofork S hg c hc).i, f'_i,
  ofIsColimitCokernelCofork_i]

Result:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : HasZeroMorphisms C
S : ShortComplex C
hg : S.g = 0
c : CokernelCofork S.f
hc : IsColimit c
⊢ S.f = S.f ≫ 𝟙 S.X₂
-- Mathlib/Topology/Order/Lattice.lean
lemma ContinuousWithinAt.finset_sup' (hne : s.Nonempty)
    (hs : ∀ i ∈ s, ContinuousWithinAt (f i) t x) : ContinuousWithinAt (s.sup' hne f) t x

Proof state:
L : Type u_1
X : Type u_2
inst✝³ : TopologicalSpace L
inst✝² : TopologicalSpace X
ι : Type u_3
inst✝¹ : SemilatticeSup L
inst✝ : ContinuousSup L
s : Finset ι
f : ι → X → L
t : Set X
x : X
hne : s.Nonempty
hs : ∀ i ∈ s, ContinuousWithinAt (f i) t x
⊢ ContinuousWithinAt (s.sup' hne f) t x

Tactic:
simpa only [← Finset.sup'_apply] using finset_sup'_apply hne hs

Result:
no goals
-- Mathlib/MeasureTheory/Constructions/BorelSpace/Order.lean
theorem borel_eq_generateFrom_Ico (α : Type*) [TopologicalSpace α] [SecondCountableTopology α]
    [LinearOrder α] [OrderTopology α] :
    borel α = .generateFrom { S : Set α | ∃ (l u : α), l < u ∧ Ico l u = S }

Proof state:
α : Type u_5
inst✝³ : TopologicalSpace α
inst✝² : SecondCountableTopology α
inst✝¹ : LinearOrder α
inst✝ : OrderTopology α
⊢ borel α = MeasurableSpace.generateFrom {S | ∃ l u, l < u ∧ Ico l u = S}

Tactic:
simpa only [exists_prop, mem_univ, true_and] using
  (@dense_univ α _).borel_eq_generateFrom_Ico_mem_aux (fun _ _ => mem_univ _) fun _ _ _ _ =>
    mem_univ _

Result:
no goals
-- Mathlib/Data/Nat/Init.lean
lemma two_le_iff : ∀ n, 2 ≤ n ↔ n ≠ 0 ∧ n ≠ 1
  | 0 => by simp
  | 1 => by simp
  | n + 2 => by simp

Proof state:
⊢ 2 ≤ 1 ↔ 1 ≠ 0 ∧ 1 ≠ 1

Tactic:
simp

Result:
no goals

Proof state:
n : ℕ
⊢ 2 ≤ n + 2 ↔ n + 2 ≠ 0 ∧ n + 2 ≠ 1

Tactic:
simp

Result:
no goals

Proof state:
⊢ 2 ≤ 0 ↔ 0 ≠ 0 ∧ 0 ≠ 1

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Group/Support.lean
theorem mulSupport_prod_mk (f : α → M) (g : α → N) :
    (mulSupport fun x => (f x, g x)) = mulSupport f ∪ mulSupport g :=
  Set.ext fun x => by
    simp only [mulSupport, not_and_or, mem_union, mem_setOf_eq, Prod.mk_eq_one, Ne]

Proof state:
α : Type u_1
M : Type u_5
N : Type u_7
inst✝¹ : One M
inst✝ : One N
f : α → M
g : α → N
x : α
⊢ (x ∈ mulSupport fun x => (f x, g x)) ↔ x ∈ mulSupport f ∪ mulSupport g

Tactic:
simp only [mulSupport, not_and_or, mem_union, mem_setOf_eq, Prod.mk_eq_one, Ne]

Result:
no goals
-- Mathlib/LinearAlgebra/SymplecticGroup.lean
theorem transpose_mem_iff : Aᵀ ∈ symplecticGroup l R ↔ A ∈ symplecticGroup l R :=
  ⟨fun hA => by simpa using transpose_mem hA, transpose_mem⟩

Proof state:
l : Type u_1
R : Type u_2
inst✝² : DecidableEq l
inst✝¹ : Fintype l
inst✝ : CommRing R
A : Matrix (l ⊕ l) (l ⊕ l) R
hA : Aᵀ ∈ symplecticGroup l R
⊢ A ∈ symplecticGroup l R

Tactic:
simpa using transpose_mem hA

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Preserves/Opposites.lean
/-- If `F : Cᵒᵖ ⥤ D` preserves finite coproducts, then `F.rightOp : C ⥤ Dᵒᵖ` preserves finite
    products. -/
lemma preservesFiniteProducts_rightOp (F : Cᵒᵖ ⥤ D) [PreservesFiniteCoproducts F] :
    PreservesFiniteProducts F.rightOp where
  preserves _

Proof state:
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : Cᵒᵖ ⥤ D
inst✝ : PreservesFiniteCoproducts F
x✝ : ℕ
⊢ PreservesLimitsOfShape (Discrete (Fin x✝)) F.rightOp

Tactic:
apply (config := { allowSynthFailures := true }) preservesLimitsOfShape_rightOp

Result:
case inst
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : Cᵒᵖ ⥤ D
inst✝ : PreservesFiniteCoproducts F
x✝ : ℕ
⊢ PreservesColimitsOfShape (Discrete (Fin x✝))ᵒᵖ F

Proof state:
case inst
C : Type u₁
inst✝² : Category.{v₁, u₁} C
D : Type u₂
inst✝¹ : Category.{v₂, u₂} D
F : Cᵒᵖ ⥤ D
inst✝ : PreservesFiniteCoproducts F
x✝ : ℕ
⊢ PreservesColimitsOfShape (Discrete (Fin x✝))ᵒᵖ F

Tactic:
exact preservesColimitsOfShape_of_equiv (Discrete.opposite _).symm _

Result:
no goals
-- Mathlib/FieldTheory/Minpoly/Field.lean
theorem isRadical [IsReduced B] : IsRadical (minpoly A x) := fun n p dvd ↦ by
  rw [dvd_iff] at dvd ⊢; rw [map_pow] at dvd; exact IsReduced.eq_zero _ ⟨n, dvd⟩

Proof state:
A : Type u_1
B : Type u_2
inst✝³ : Field A
inst✝² : Ring B
inst✝¹ : Algebra A B
x : B
inst✝ : IsReduced B
n : ℕ
p : A[X]
dvd : (Polynomial.aeval x) p ^ n = 0
⊢ (Polynomial.aeval x) p = 0

Tactic:
exact IsReduced.eq_zero _ ⟨n, dvd⟩

Result:
no goals

Proof state:
A : Type u_1
B : Type u_2
inst✝³ : Field A
inst✝² : Ring B
inst✝¹ : Algebra A B
x : B
inst✝ : IsReduced B
n : ℕ
p : A[X]
dvd : minpoly A x ∣ p ^ n
⊢ minpoly A x ∣ p

Tactic:
rw [dvd_iff] at dvd ⊢

Result:
A : Type u_1
B : Type u_2
inst✝³ : Field A
inst✝² : Ring B
inst✝¹ : Algebra A B
x : B
inst✝ : IsReduced B
n : ℕ
p : A[X]
dvd : (Polynomial.aeval x) (p ^ n) = 0
⊢ (Polynomial.aeval x) p = 0

Proof state:
A : Type u_1
B : Type u_2
inst✝³ : Field A
inst✝² : Ring B
inst✝¹ : Algebra A B
x : B
inst✝ : IsReduced B
n : ℕ
p : A[X]
dvd : (Polynomial.aeval x) (p ^ n) = 0
⊢ (Polynomial.aeval x) p = 0

Tactic:
rw [map_pow] at dvd

Result:
A : Type u_1
B : Type u_2
inst✝³ : Field A
inst✝² : Ring B
inst✝¹ : Algebra A B
x : B
inst✝ : IsReduced B
n : ℕ
p : A[X]
dvd : (Polynomial.aeval x) p ^ n = 0
⊢ (Polynomial.aeval x) p = 0
-- Mathlib/Topology/Algebra/ContinuousMonoidHom.lean
theorem toContinuousMap_injective : Injective (toContinuousMap : _ → C(A, B)) := fun f g h =>
  ext <| by convert DFunLike.ext_iff.1 h

Proof state:
A : Type u_2
B : Type u_3
inst✝³ : Monoid A
inst✝² : Monoid B
inst✝¹ : TopologicalSpace A
inst✝ : TopologicalSpace B
f g : ContinuousMonoidHom A B
h : f.toContinuousMap = g.toContinuousMap
⊢ ∀ (x : A), f x = g x

Tactic:
convert DFunLike.ext_iff.1 h

Result:
no goals
-- Mathlib/MeasureTheory/Function/LpSpace/Basic.lean
theorem smul_compLpL [Fact (1 ≤ p)] {𝕜'} [NormedRing 𝕜'] [Module 𝕜' F] [BoundedSMul 𝕜' F]
    [SMulCommClass 𝕜 𝕜' F] (c : 𝕜') (L : E →L[𝕜] F) : (c • L).compLpL p μ = c • L.compLpL p μ

Proof state:
α : Type u_1
E : Type u_4
F : Type u_5
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedAddCommGroup F
𝕜 : Type u_7
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : NormedSpace 𝕜 F
inst✝⁴ : Fact (1 ≤ p)
𝕜' : Type u_8
inst✝³ : NormedRing 𝕜'
inst✝² : Module 𝕜' F
inst✝¹ : BoundedSMul 𝕜' F
inst✝ : SMulCommClass 𝕜 𝕜' F
c : 𝕜'
L : E →L[𝕜] F
⊢ compLpL p μ (c • L) = c • compLpL p μ L

Tactic:
ext1 f

Result:
case h
α : Type u_1
E : Type u_4
F : Type u_5
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedAddCommGroup F
𝕜 : Type u_7
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : NormedSpace 𝕜 F
inst✝⁴ : Fact (1 ≤ p)
𝕜' : Type u_8
inst✝³ : NormedRing 𝕜'
inst✝² : Module 𝕜' F
inst✝¹ : BoundedSMul 𝕜' F
inst✝ : SMulCommClass 𝕜 𝕜' F
c : 𝕜'
L : E →L[𝕜] F
f : ↥(Lp E p μ)
⊢ (compLpL p μ (c • L)) f = (c • compLpL p μ L) f

Proof state:
case h
α : Type u_1
E : Type u_4
F : Type u_5
m0 : MeasurableSpace α
p : ℝ≥0∞
μ : Measure α
inst✝⁹ : NormedAddCommGroup E
inst✝⁸ : NormedAddCommGroup F
𝕜 : Type u_7
inst✝⁷ : NontriviallyNormedField 𝕜
inst✝⁶ : NormedSpace 𝕜 E
inst✝⁵ : NormedSpace 𝕜 F
inst✝⁴ : Fact (1 ≤ p)
𝕜' : Type u_8
inst✝³ : NormedRing 𝕜'
inst✝² : Module 𝕜' F
inst✝¹ : BoundedSMul 𝕜' F
inst✝ : SMulCommClass 𝕜 𝕜' F
c : 𝕜'
L : E →L[𝕜] F
f : ↥(Lp E p μ)
⊢ (compLpL p μ (c • L)) f = (c • compLpL p μ L) f

Tactic:
exact smul_compLp c L f

Result:
no goals
-- Mathlib/Dynamics/PeriodicPts/Defs.lean
theorem const_mul (hm : IsPeriodicPt f m x) (n : ℕ) : IsPeriodicPt f (n * m) x

Proof state:
α : Type u_1
f : α → α
x : α
m : ℕ
hm : IsPeriodicPt f m x
n : ℕ
⊢ IsPeriodicPt f (n * m) x

Tactic:
simp only [mul_comm n, hm.mul_const n]

Result:
no goals
-- Mathlib/AlgebraicGeometry/RationalMap.lean
lemma restrict_id_hom (f : X.PartialMap Y) :
    (f.restrict f.domain f.dense_domain le_rfl).hom = f.hom

Proof state:
X Y : Scheme
f : X.PartialMap Y
⊢ (f.restrict f.domain ⋯ ⋯).hom = f.hom

Tactic:
simp

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Option/Attach.lean
theorem bind_subtype {p : α → Prop} {o : Option { x // p x }}
    {f : { x // p x } → Option β} {g : α → Option β} (hf : ∀ x h, f ⟨x, h⟩ = g x) :
    (o.bind f) = o.unattach.bind g

Proof state:
α : Type u_1
β : Type u_2
p : α → Prop
o : Option { x // p x }
f : { x // p x } → Option β
g : α → Option β
hf : ∀ (x : α) (h : p x), f ⟨x, h⟩ = g x
⊢ o.bind f = o.unattach.bind g

Tactic:
cases o <;> simp [hf]

Result:
no goals
-- Mathlib/Data/Rat/Cast/Order.lean
theorem cast_lt_natCast {m : ℚ≥0} {n : ℕ} : (m : K) < n ↔ m < (n : ℚ≥0)

Proof state:
K : Type u_5
inst✝ : LinearOrderedSemifield K
m : ℚ≥0
n : ℕ
⊢ ↑m < ↑n ↔ m < ↑n

Tactic:
rw [← cast_lt (K := K), cast_natCast]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Jacobian.lean
lemma baseChange_nonsingular (hf : Function.Injective f) (P : Fin 3 → A) :
    (W'.baseChange B).toJacobian.Nonsingular (f ∘ P) ↔
      (W'.baseChange A).toJacobian.Nonsingular P

Proof state:
R : Type r
inst✝¹⁰ : CommRing R
W' : Jacobian R
S : Type s
inst✝⁹ : CommRing S
inst✝⁸ : Algebra R S
A : Type u
inst✝⁷ : CommRing A
inst✝⁶ : Algebra R A
inst✝⁵ : Algebra S A
inst✝⁴ : IsScalarTower R S A
B : Type v
inst✝³ : CommRing B
inst✝² : Algebra R B
inst✝¹ : Algebra S B
inst✝ : IsScalarTower R S B
f : A →ₐ[S] B
hf : Function.Injective ⇑f
P : Fin 3 → A
⊢ (baseChange W' B).toJacobian.Nonsingular (⇑f ∘ P) ↔ (baseChange W' A).toJacobian.Nonsingular P

Tactic:
rw [← RingHom.coe_coe, ← map_nonsingular hf, AlgHom.toRingHom_eq_coe, map_baseChange]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Gcd.lean
theorem gcd_self (n : Nat) : gcd n n = n

Proof state:
n : Nat
⊢ n.gcd n = n

Tactic:
cases n <;> simp [gcd_succ]

Result:
no goals
-- Mathlib/Data/Real/EReal.lean
theorem coe_toReal {x : EReal} (hx : x ≠ ⊤) (h'x : x ≠ ⊥) : (x.toReal : EReal) = x

Proof state:
case intro
x : ℝ
hx : ↑x ≠ ⊤
h'x : ↑x ≠ ⊥
⊢ ↑(↑x).toReal = ↑x

Tactic:
rfl

Result:
no goals

Proof state:
x : EReal
hx : x ≠ ⊤
h'x : x ≠ ⊥
⊢ ↑x.toReal = x

Tactic:
lift x to ℝ using ⟨hx, h'x⟩

Result:
case intro
x : ℝ
hx : ↑x ≠ ⊤
h'x : ↑x ≠ ⊥
⊢ ↑(↑x).toReal = ↑x
-- Mathlib/AlgebraicTopology/SimplicialObject/Basic.lean
theorem σ_comp_σ {n} {i j : Fin (n + 1)} (H : i ≤ j) :
    X.σ (Fin.castSucc i) ≫ X.σ j = X.σ j.succ ≫ X.σ i

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X : CosimplicialObject C
n : ℕ
i j : Fin (n + 1)
H : i ≤ j
⊢ X.map (SimplexCategory.σ i.castSucc) ≫ X.map (SimplexCategory.σ j) =
    X.map (SimplexCategory.σ j.succ) ≫ X.map (SimplexCategory.σ i)

Tactic:
simp only [← X.map_comp, SimplexCategory.σ_comp_σ H]

Result:
no goals

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X : CosimplicialObject C
n : ℕ
i j : Fin (n + 1)
H : i ≤ j
⊢ X.σ i.castSucc ≫ X.σ j = X.σ j.succ ≫ X.σ i

Tactic:
dsimp [δ, σ]

Result:
C : Type u
inst✝ : Category.{v, u} C
X : CosimplicialObject C
n : ℕ
i j : Fin (n + 1)
H : i ≤ j
⊢ X.map (SimplexCategory.σ i.castSucc) ≫ X.map (SimplexCategory.σ j) =
    X.map (SimplexCategory.σ j.succ) ≫ X.map (SimplexCategory.σ i)
-- Mathlib/Algebra/Homology/HomotopyCofiber.lean
@[reassoc (attr := simp)]
lemma inlX_fstX (i j : ι ) (hij : c.Rel j i) :
    inlX φ i j hij ≫ fstX φ j i hij = 𝟙 _

Proof state:
C : Type u_1
inst✝³ : Category.{u_3, u_1} C
inst✝² : Preadditive C
ι : Type u_2
c : ComplexShape ι
F G : HomologicalComplex C c
φ : F ⟶ G
inst✝¹ : HasHomotopyCofiber φ
inst✝ : DecidableRel c.Rel
i j : ι
hij : c.Rel j i
⊢ inlX φ i j hij ≫ fstX φ j i hij = 𝟙 (F.X i)

Tactic:
simp [inlX, fstX]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem getElem?_eq {a : Array α} {i : Nat} :
    a[i]? = if h : i < a.size then some a[i] else none

Proof state:
α : Type u_1
a : Array α
i : Nat
⊢ a[i]? = if h : i < a.size then some a[i] else none

Tactic:
rw [getElem?_def]

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Projective.lean
lemma baseChange_dblU (P : Fin 3 → F) : (W'.baseChange K).toProjective.dblU (f ∘ P) =
    f ((W'.baseChange F).toProjective.dblU P)

Proof state:
F : Type u
inst✝¹⁰ : Field F
R : Type r
inst✝⁹ : CommRing R
W' : Projective R
S : Type s
inst✝⁸ : CommRing S
inst✝⁷ : Algebra R S
inst✝⁶ : Algebra R F
inst✝⁵ : Algebra S F
inst✝⁴ : IsScalarTower R S F
K : Type v
inst✝³ : Field K
inst✝² : Algebra R K
inst✝¹ : Algebra S K
inst✝ : IsScalarTower R S K
f : F →ₐ[S] K
P : Fin 3 → F
⊢ (baseChange W' K).toProjective.dblU (⇑f ∘ P) = f ((baseChange W' F).toProjective.dblU P)

Tactic:
rw [← RingHom.coe_coe, ← map_dblU, map_baseChange]

Result:
no goals
-- Mathlib/Topology/Basic.lean
theorem closure_nonempty_iff : (closure s).Nonempty ↔ s.Nonempty

Proof state:
X : Type u
s : Set X
inst✝ : TopologicalSpace X
⊢ (closure s).Nonempty ↔ s.Nonempty

Tactic:
simp only [nonempty_iff_ne_empty, Ne, closure_empty_iff]

Result:
no goals
-- Mathlib/Topology/Order/LeftRightNhds.lean
theorem nhds_basis_zero_abs_sub_lt [NoMaxOrder α] :
    (𝓝 (0 : α)).HasBasis (fun ε : α => (0 : α) < ε) fun ε => { b | |b| < ε }

Proof state:
α : Type u_1
inst✝³ : TopologicalSpace α
inst✝² : LinearOrderedAddCommGroup α
inst✝¹ : OrderTopology α
inst✝ : NoMaxOrder α
⊢ (𝓝 0).HasBasis (fun ε => 0 < ε) fun ε => {b | |b| < ε}

Tactic:
simpa using nhds_basis_abs_sub_lt (0 : α)

Result:
no goals
-- Mathlib/Data/Nat/Init.lean
protected lemma eq_sub_of_add_eq' (h : b + c = a) : c = a - b

Proof state:
a b c : ℕ
h : b + c = a
⊢ c = a - b

Tactic:
omega

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Restrict.lean
theorem restrict_apply_univ (s : Set α) : μ.restrict s univ = μ s

Proof state:
α : Type u_2
m0 : MeasurableSpace α
μ : Measure α
s : Set α
⊢ (μ.restrict s) univ = μ s

Tactic:
rw [restrict_apply MeasurableSet.univ, Set.univ_inter]

Result:
no goals
-- Mathlib/RepresentationTheory/GroupCohomology/LowDegree.lean
theorem isMulOneCoboundary_of_mem_oneCoboundaries
    (f : G → M) (hf : f ∈ oneCoboundaries (Rep.ofMulDistribMulAction G M)) :
    IsMulOneCoboundary (M := M) (Additive.ofMul ∘ f)

Proof state:
case intro
G M : Type
inst✝² : Group G
inst✝¹ : CommGroup M
inst✝ : MulDistribMulAction G M
x : ↑(Rep.ofMulDistribMulAction G M).V
⊢ IsMulOneCoboundary (⇑Additive.ofMul ∘ (dZero (Rep.ofMulDistribMulAction G M)) x)

Tactic:
exact ⟨x, fun _ =>  rfl⟩

Result:
no goals

Proof state:
G M : Type
inst✝² : Group G
inst✝¹ : CommGroup M
inst✝ : MulDistribMulAction G M
f : G → M
hf : f ∈ oneCoboundaries (Rep.ofMulDistribMulAction G M)
⊢ IsMulOneCoboundary (⇑Additive.ofMul ∘ f)

Tactic:
rcases hf with ⟨x, rfl⟩

Result:
case intro
G M : Type
inst✝² : Group G
inst✝¹ : CommGroup M
inst✝ : MulDistribMulAction G M
x : ↑(Rep.ofMulDistribMulAction G M).V
⊢ IsMulOneCoboundary (⇑Additive.ofMul ∘ (dZero (Rep.ofMulDistribMulAction G M)) x)
-- Mathlib/RingTheory/AdicCompletion/AsTensorProduct.lean
private
lemma ofTensorProduct_bijective_of_map_from_fin [Fintype ι] [IsNoetherianRing R] :
    Function.Bijective (ofTensorProduct I M)

Proof state:
R : Type u
inst✝⁴ : CommRing R
I : Ideal R
M : Type u
inst✝³ : AddCommGroup M
inst✝² : Module R M
ι : Type
f : (ι → R) →ₗ[R] M
hf : Function.Surjective ⇑f
inst✝¹ : Fintype ι
inst✝ : IsNoetherianRing R
this : IsIso (ModuleCat.ofHom (ofTensorProduct I M))
⊢ Function.Bijective ⇑(ofTensorProduct I M)

Tactic:
exact ConcreteCategory.bijective_of_isIso (ModuleCat.ofHom (ofTensorProduct I M))

Result:
no goals

Proof state:
R : Type u
inst✝⁴ : CommRing R
I : Ideal R
M : Type u
inst✝³ : AddCommGroup M
inst✝² : Module R M
ι : Type
f : (ι → R) →ₗ[R] M
hf : Function.Surjective ⇑f
inst✝¹ : Fintype ι
inst✝ : IsNoetherianRing R
⊢ Function.Bijective ⇑(ofTensorProduct I M)

Tactic:
have : IsIso (ModuleCat.ofHom (ofTensorProduct I M)) :=
  ofTensorProduct_iso I M f hf

Result:
R : Type u
inst✝⁴ : CommRing R
I : Ideal R
M : Type u
inst✝³ : AddCommGroup M
inst✝² : Module R M
ι : Type
f : (ι → R) →ₗ[R] M
hf : Function.Surjective ⇑f
inst✝¹ : Fintype ι
inst✝ : IsNoetherianRing R
this : IsIso (ModuleCat.ofHom (ofTensorProduct I M))
⊢ Function.Bijective ⇑(ofTensorProduct I M)
-- Mathlib/FieldTheory/Separable.lean
theorem separable_C (r : R) : (C r).Separable ↔ IsUnit r

Proof state:
R : Type u
inst✝ : CommSemiring R
r : R
⊢ (C r).Separable ↔ IsUnit r

Tactic:
rw [separable_def, derivative_C, isCoprime_zero_right, isUnit_C]

Result:
no goals
-- Mathlib/Algebra/MonoidAlgebra/Defs.lean
theorem liftNC_one {g_hom : Type*} [FunLike g_hom G R] [OneHomClass g_hom G R]
    (f : k →+* R) (g : g_hom) :
    liftNC (f : k →+ R) g 1 = 1

Proof state:
k : Type u₁
G : Type u₂
R : Type u_2
inst✝⁴ : NonAssocSemiring R
inst✝³ : Semiring k
inst✝² : One G
g_hom : Type u_3
inst✝¹ : FunLike g_hom G R
inst✝ : OneHomClass g_hom G R
f : k →+* R
g : g_hom
⊢ (liftNC ↑f ⇑g) 1 = 1

Tactic:
simp [one_def]

Result:
no goals
-- Mathlib/Dynamics/TopologicalEntropy/DynamicalEntourage.lean
@[simp]
lemma dynEntourage_one {T : X → X} {U : Set (X × X)} :
    dynEntourage T U 1 = U

Proof state:
X : Type u_1
T : X → X
U : Set (X × X)
⊢ dynEntourage T U 1 = U

Tactic:
simp [dynEntourage]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/DivModLemmas.lean
theorem emod_add_emod (m n k : Int) : (m % n + k) % n = (m + k) % n

Proof state:
m n k : Int
⊢ (m % n + k) % n = (m + k) % n

Tactic:
have := (add_mul_emod_self_left (m % n + k) n (m / n)).symm

Result:
m n k : Int
this : (m % n + k) % n = (m % n + k + n * (m / n)) % n
⊢ (m % n + k) % n = (m + k) % n

Proof state:
m n k : Int
this : (m % n + k) % n = (m % n + k + n * (m / n)) % n
⊢ (m % n + k) % n = (m + k) % n

Tactic:
rwa [Int.add_right_comm, emod_add_ediv] at this

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem toList_shrink (a : Array α) (n : Nat) : (a.shrink n).toList = a.toList.take n

Proof state:
α : Type u_1
a : Array α
n : Nat
⊢ (a.shrink n).toList = List.take n a.toList

Tactic:
apply List.ext_getElem <;> simp

Result:
no goals
-- Mathlib/Algebra/Group/Even.lean
@[to_additive]
lemma IsSquare.mul [CommSemigroup α] {a b : α} : IsSquare a → IsSquare b → IsSquare (a * b)

Proof state:
case intro.intro
α : Type u_2
inst✝ : CommSemigroup α
r s : α
⊢ IsSquare (r * r * (s * s))

Tactic:
exact ⟨r * s, mul_mul_mul_comm _ _ _ _⟩

Result:
no goals

Proof state:
α : Type u_2
inst✝ : CommSemigroup α
a b : α
⊢ IsSquare a → IsSquare b → IsSquare (a * b)

Tactic:
rintro ⟨r, rfl⟩ ⟨s, rfl⟩

Result:
case intro.intro
α : Type u_2
inst✝ : CommSemigroup α
r s : α
⊢ IsSquare (r * r * (s * s))
-- Mathlib/InformationTheory/Hamming.lean
theorem hammingNorm_comp_le_hammingNorm (f : ∀ i, γ i → β i) {x : ∀ i, γ i} (hf : ∀ i, f i 0 = 0) :
    (hammingNorm fun i => f i (x i)) ≤ hammingNorm x

Proof state:
ι : Type u_2
β : ι → Type u_3
inst✝⁴ : Fintype ι
inst✝³ : (i : ι) → DecidableEq (β i)
γ : ι → Type u_4
inst✝² : (i : ι) → DecidableEq (γ i)
inst✝¹ : (i : ι) → Zero (β i)
inst✝ : (i : ι) → Zero (γ i)
f : (i : ι) → γ i → β i
x : (i : ι) → γ i
hf : ∀ (i : ι), f i 0 = 0
⊢ (hammingNorm fun i => f i (x i)) ≤ hammingNorm x

Tactic:
simpa only [← hammingDist_zero_right, hf] using hammingDist_comp_le_hammingDist f (y := fun _ ↦ 0)

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/Block.lean
theorem twoBlockTriangular_det' (M : Matrix m m R) (p : m → Prop) [DecidablePred p]
    (h : ∀ i, p i → ∀ j, ¬p j → M i j = 0) :
    M.det = (toSquareBlockProp M p).det * (toSquareBlockProp M fun i => ¬p i).det

Proof state:
m : Type u_3
R : Type v
inst✝³ : CommRing R
inst✝² : DecidableEq m
inst✝¹ : Fintype m
M : Matrix m m R
p : m → Prop
inst✝ : DecidablePred p
h : ∀ (i : m), p i → ∀ (j : m), ¬p j → M i j = 0
⊢ (M.toSquareBlockProp fun i => ¬¬p i).det * (M.toSquareBlockProp fun i => ¬p i).det =
    (M.toSquareBlockProp p).det * (M.toSquareBlockProp fun i => ¬p i).det

Tactic:
congr 1

Result:
case e_a
m : Type u_3
R : Type v
inst✝³ : CommRing R
inst✝² : DecidableEq m
inst✝¹ : Fintype m
M : Matrix m m R
p : m → Prop
inst✝ : DecidablePred p
h : ∀ (i : m), p i → ∀ (j : m), ¬p j → M i j = 0
⊢ (M.toSquareBlockProp fun i => ¬¬p i).det = (M.toSquareBlockProp p).det

Proof state:
m : Type u_3
R : Type v
inst✝³ : CommRing R
inst✝² : DecidableEq m
inst✝¹ : Fintype m
M : Matrix m m R
p : m → Prop
inst✝ : DecidablePred p
h : ∀ (i : m), p i → ∀ (j : m), ¬p j → M i j = 0
⊢ ∀ (i : m), ¬¬p i → ∀ (j : m), ¬p j → M i j = 0

Tactic:
simpa only [Classical.not_not] using h

Result:
no goals

Proof state:
case e_a
m : Type u_3
R : Type v
inst✝³ : CommRing R
inst✝² : DecidableEq m
inst✝¹ : Fintype m
M : Matrix m m R
p : m → Prop
inst✝ : DecidablePred p
h : ∀ (i : m), p i → ∀ (j : m), ¬p j → M i j = 0
⊢ (M.toSquareBlockProp fun i => ¬¬p i).det = (M.toSquareBlockProp p).det

Tactic:
exact equiv_block_det _ fun _ => not_not.symm

Result:
no goals

Proof state:
m : Type u_3
R : Type v
inst✝³ : CommRing R
inst✝² : DecidableEq m
inst✝¹ : Fintype m
M : Matrix m m R
p : m → Prop
inst✝ : DecidablePred p
h : ∀ (i : m), p i → ∀ (j : m), ¬p j → M i j = 0
⊢ M.det = (M.toSquareBlockProp p).det * (M.toSquareBlockProp fun i => ¬p i).det

Tactic:
rw [M.twoBlockTriangular_det fun i => ¬p i, mul_comm]

Result:
m : Type u_3
R : Type v
inst✝³ : CommRing R
inst✝² : DecidableEq m
inst✝¹ : Fintype m
M : Matrix m m R
p : m → Prop
inst✝ : DecidablePred p
h : ∀ (i : m), p i → ∀ (j : m), ¬p j → M i j = 0
⊢ (M.toSquareBlockProp fun i => ¬¬p i).det * (M.toSquareBlockProp fun i => ¬p i).det =
    (M.toSquareBlockProp p).det * (M.toSquareBlockProp fun i => ¬p i).det

m : Type u_3
R : Type v
inst✝³ : CommRing R
inst✝² : DecidableEq m
inst✝¹ : Fintype m
M : Matrix m m R
p : m → Prop
inst✝ : DecidablePred p
h : ∀ (i : m), p i → ∀ (j : m), ¬p j → M i j = 0
⊢ ∀ (i : m), ¬¬p i → ∀ (j : m), ¬p j → M i j = 0