harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Algebra/MvPolynomial/Rename.lean
theorem rename_eq (f : σ → τ) (p : MvPolynomial σ R) :
    rename f p = Finsupp.mapDomain (Finsupp.mapDomain f) p

Proof state:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst✝ : CommSemiring R
f : σ → τ
p : MvPolynomial σ R
⊢ (sum p fun s a => (monomial (s.sum fun a => Finsupp.single (f a))) a) =
    sum p fun a => Finsupp.single (a.sum fun a => Finsupp.single (f a))

Tactic:
rfl

Result:
no goals

Proof state:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst✝ : CommSemiring R
f : σ → τ
p : MvPolynomial σ R
⊢ (rename f) p = Finsupp.mapDomain (Finsupp.mapDomain f) p

Tactic:
simp only [rename, aeval_def, eval₂, Finsupp.mapDomain, algebraMap_eq, comp_apply,
  X_pow_eq_monomial, ← monomial_finsupp_sum_index]

Result:
σ : Type u_1
τ : Type u_2
R : Type u_4
inst✝ : CommSemiring R
f : σ → τ
p : MvPolynomial σ R
⊢ (sum p fun s a => (monomial (s.sum fun a => Finsupp.single (f a))) a) =
    sum p fun a => Finsupp.single (a.sum fun a => Finsupp.single (f a))
-- Mathlib/CategoryTheory/Limits/Preserves/Shapes/Kernels.lean
theorem kernel_map_comp_preserves_kernel_iso_inv {X' Y' : C} (g : X' ⟶ Y') [HasKernel g]
    [HasKernel (G.map g)] [PreservesLimit (parallelPair g 0) G] (p : X ⟶ X') (q : Y ⟶ Y')
    (hpq : f ≫ q = p ≫ g) :
    kernel.map (G.map f) (G.map g) (G.map p) (G.map q) (by rw [← G.map_comp, hpq, G.map_comp]) ≫
        (PreservesKernel.iso G _).inv =
      (PreservesKernel.iso G _).inv ≫ G.map (kernel.map f g p q hpq)

Proof state:
C : Type u₁
inst✝¹⁰ : Category.{v₁, u₁} C
inst✝⁹ : HasZeroMorphisms C
D : Type u₂
inst✝⁸ : Category.{v₂, u₂} D
inst✝⁷ : HasZeroMorphisms D
G : C ⥤ D
inst✝⁶ : G.PreservesZeroMorphisms
X Y Z : C
f : X ⟶ Y
h : Z ⟶ X
w : h ≫ f = 0
inst✝⁵ : HasKernel f
inst✝⁴ : HasKernel (G.map f)
inst✝³ : PreservesLimit (parallelPair f 0) G
X' Y' : C
g : X' ⟶ Y'
inst✝² : HasKernel g
inst✝¹ : HasKernel (G.map g)
inst✝ : PreservesLimit (parallelPair g 0) G
p : X ⟶ X'
q : Y ⟶ Y'
hpq : f ≫ q = p ≫ g
⊢ G.map f ≫ G.map q = G.map p ≫ G.map g

Tactic:
rw [← G.map_comp, hpq, G.map_comp]

Result:
no goals

Proof state:
C : Type u₁
inst✝¹⁰ : Category.{v₁, u₁} C
inst✝⁹ : HasZeroMorphisms C
D : Type u₂
inst✝⁸ : Category.{v₂, u₂} D
inst✝⁷ : HasZeroMorphisms D
G : C ⥤ D
inst✝⁶ : G.PreservesZeroMorphisms
X Y : C
f : X ⟶ Y
inst✝⁵ : HasKernel f
inst✝⁴ : HasKernel (G.map f)
inst✝³ : PreservesLimit (parallelPair f 0) G
X' Y' : C
g : X' ⟶ Y'
inst✝² : HasKernel g
inst✝¹ : HasKernel (G.map g)
inst✝ : PreservesLimit (parallelPair g 0) G
p : X ⟶ X'
q : Y ⟶ Y'
hpq : f ≫ q = p ≫ g
⊢ kernel.map (G.map f) (G.map g) (G.map p) (G.map q) ⋯ ≫ (PreservesKernel.iso G g).inv =
    (PreservesKernel.iso G f).inv ≫ G.map (kernel.map f g p q hpq)

Tactic:
rw [Iso.comp_inv_eq, Category.assoc, PreservesKernel.iso_hom, Iso.eq_inv_comp,
  PreservesKernel.iso_hom, kernelComparison_comp_kernel_map]

Result:
no goals
-- Mathlib/NumberTheory/Divisors.lean
theorem swap_mem_divisorsAntidiagonal_aux {x : ℕ × ℕ} :
    x.snd * x.fst = n ∧ ¬n = 0 ↔ x ∈ divisorsAntidiagonal n

Proof state:
n : ℕ
x : ℕ × ℕ
⊢ x.2 * x.1 = n ∧ ¬n = 0 ↔ x ∈ n.divisorsAntidiagonal

Tactic:
rw [mem_divisorsAntidiagonal, mul_comm]

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/Pullback/CommSq.lean
theorem of_is_coproduct {c : BinaryCofan X Y} (h : Limits.IsColimit c) (t : IsInitial Z) :
    IsPushout (t.to _) (t.to _) c.inl c.inr :=
  of_isColimit
    (isPushoutOfIsInitialIsCoproduct _ _ _ _ t
      (IsColimit.ofIsoColimit h
        (Limits.Cocones.ext (Iso.refl c.pt)
          (by
            rintro ⟨⟨⟩⟩ <;>
              · dsimp
                simp))))

Proof state:
case mk.right
C : Type u₁
inst✝ : Category.{v₁, u₁} C
Z X Y : C
c : BinaryCofan X Y
h : IsColimit c
t : IsInitial Z
⊢ c.inr ≫ 𝟙 c.pt = c.inr

Tactic:
simp

Result:
no goals

Proof state:
case mk.right
C : Type u₁
inst✝ : Category.{v₁, u₁} C
Z X Y : C
c : BinaryCofan X Y
h : IsColimit c
t : IsInitial Z
⊢ c.ι.app { as := WalkingPair.right } ≫ (Iso.refl c.pt).hom =
    (BinaryCofan.mk (c.ι.1 { as := WalkingPair.left }) (c.ι.1 { as := WalkingPair.right })).ι.app
      { as := WalkingPair.right }

Tactic:
dsimp

Result:
case mk.right
C : Type u₁
inst✝ : Category.{v₁, u₁} C
Z X Y : C
c : BinaryCofan X Y
h : IsColimit c
t : IsInitial Z
⊢ c.inr ≫ 𝟙 c.pt = c.inr
-- Mathlib/Topology/OmegaCompletePartialOrder.lean
lemma scott_eq_Scott {α} [OmegaCompletePartialOrder α] :
    Topology.scott α (Set.range fun c : Chain α => Set.range c) = Scott.topologicalSpace α

Proof state:
case a.h.a
α : Type u_1
inst✝ : OmegaCompletePartialOrder α
U : Set α
this : TopologicalSpace α := Topology.scott α (range fun c => range ⇑c)
⊢ IsOpen U ↔ IsOpen U

Tactic:
rw [isOpen_iff_ωScottContinuous_mem, @isOpen_iff_continuous_mem,
  @Topology.IsScott.ωscottContinuous_iff_continuous _ _
    (Topology.scott α (Set.range fun c : Chain α => Set.range c)) ({ topology_eq_scott := rfl })]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : OmegaCompletePartialOrder α
⊢ Topology.scott α (range fun c => range ⇑c) = Scott.topologicalSpace α

Tactic:
ext U

Result:
case a.h.a
α : Type u_1
inst✝ : OmegaCompletePartialOrder α
U : Set α
⊢ IsOpen U ↔ IsOpen U

Proof state:
case a.h.a
α : Type u_1
inst✝ : OmegaCompletePartialOrder α
U : Set α
⊢ IsOpen U ↔ IsOpen U

Tactic:
letI := Topology.scott α (Set.range fun c : Chain α => Set.range c)

Result:
case a.h.a
α : Type u_1
inst✝ : OmegaCompletePartialOrder α
U : Set α
this : TopologicalSpace α := Topology.scott α (range fun c => range ⇑c)
⊢ IsOpen U ↔ IsOpen U
-- Mathlib/RingTheory/FractionalIdeal/Basic.lean
theorem coeIdeal_mul (I J : Ideal R) : (↑(I * J) : FractionalIdeal S P) = I * J

Proof state:
R : Type u_1
inst✝² : CommRing R
S : Submonoid R
P : Type u_2
inst✝¹ : CommRing P
inst✝ : Algebra R P
I J : Ideal R
⊢ ↑(I * J) = ↑I * ↑J

Tactic:
simp only [mul_def]

Result:
R : Type u_1
inst✝² : CommRing R
S : Submonoid R
P : Type u_2
inst✝¹ : CommRing P
inst✝ : Algebra R P
I J : Ideal R
⊢ ↑(I * J) = ⟨↑↑I * ↑↑J, ⋯⟩

Proof state:
R : Type u_1
inst✝² : CommRing R
S : Submonoid R
P : Type u_2
inst✝¹ : CommRing P
inst✝ : Algebra R P
I J : Ideal R
⊢ ↑(I * J) = ⟨↑↑I * ↑↑J, ⋯⟩

Tactic:
exact coeToSubmodule_injective (coeSubmodule_mul _ _ _)

Result:
no goals
-- Mathlib/Algebra/Polynomial/Basic.lean
theorem erase_same (p : R[X]) (n : ℕ) : coeff (p.erase n) n = 0

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
n : ℕ
⊢ (erase n p).coeff n = 0

Tactic:
simp [coeff_erase]

Result:
no goals
-- Mathlib/MeasureTheory/Function/SimpleFuncDenseLp.lean
theorem norm_toSimpleFunc [Fact (1 ≤ p)] (f : Lp.simpleFunc E p μ) :
    ‖f‖ = ENNReal.toReal (eLpNorm (toSimpleFunc f) p μ)

Proof state:
α : Type u_1
E : Type u_4
inst✝² : MeasurableSpace α
inst✝¹ : NormedAddCommGroup E
p : ℝ≥0∞
μ : Measure α
inst✝ : Fact (1 ≤ p)
f : ↥(simpleFunc E p μ)
⊢ ‖f‖ = (eLpNorm (⇑(toSimpleFunc f)) p μ).toReal

Tactic:
simpa [toLp_toSimpleFunc] using norm_toLp (toSimpleFunc f) (simpleFunc.memLp f)

Result:
no goals
-- Mathlib/Algebra/Polynomial/Reverse.lean
@[simp] lemma reflect_one_X : reflect 1 (X : R[X]) = 1

Proof state:
R : Type u_1
inst✝ : Semiring R
⊢ reflect 1 X = 1

Tactic:
simpa using reflect_monomial 1 1 (R := R)

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/List/Associative.lean
theorem length_insertEntry [BEq α] {l : List ((a : α) × β a)} {k : α} {v : β k} :
    (insertEntry k v l).length = if containsKey k l then l.length else l.length + 1

Proof state:
α : Type u
β : α → Type v
inst✝ : BEq α
l : List ((a : α) × β a)
k : α
v : β k
⊢ (insertEntry k v l).length = if containsKey k l = true then l.length else l.length + 1

Tactic:
simp [insertEntry, Bool.apply_cond List.length]

Result:
no goals
-- Mathlib/Order/SuccPred/Limit.lean
theorem isLUB_Iio_iff_isSuccPrelimit : IsLUB (Iio a) a ↔ IsSuccPrelimit a

Proof state:
α : Type u_1
inst✝ : LinearOrder α
b : α
ha : IsLUB (Iic b) b
hb : b ⋖ b
⊢ False

Tactic:
cases hb.lt.false

Result:
no goals

Proof state:
α : Type u_1
a : α
inst✝ : LinearOrder α
b : α
ha : IsLUB (Iic b) a
hb : b ⋖ a
⊢ False

Tactic:
obtain rfl := isLUB_Iic.unique ha

Result:
α : Type u_1
inst✝ : LinearOrder α
b : α
ha : IsLUB (Iic b) b
hb : b ⋖ b
⊢ False

Proof state:
α : Type u_1
a : α
inst✝ : LinearOrder α
⊢ IsLUB (Iio a) a ↔ IsSuccPrelimit a

Tactic:
refine ⟨fun ha b hb ↦ ?_, IsSuccPrelimit.isLUB_Iio⟩

Result:
α : Type u_1
a : α
inst✝ : LinearOrder α
ha : IsLUB (Iio a) a
b : α
hb : b ⋖ a
⊢ False

Proof state:
α : Type u_1
a : α
inst✝ : LinearOrder α
ha : IsLUB (Iio a) a
b : α
hb : b ⋖ a
⊢ False

Tactic:
rw [hb.Iio_eq] at ha

Result:
α : Type u_1
a : α
inst✝ : LinearOrder α
b : α
ha : IsLUB (Iic b) a
hb : b ⋖ a
⊢ False
-- Mathlib/Tactic/Abel.lean
theorem const_add_termg {α} [AddCommGroup α] (k n x a a') (h : k + a = a') :
    k + @termg α _ n x a = termg n x a'

Proof state:
α : Type u_1
inst✝ : AddCommGroup α
k : α
n : ℤ
x a a' : α
h : k + a = a'
⊢ k + termg n x a = termg n x a'

Tactic:
simp [h.symm, termg, add_comm, add_assoc]

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/Orientation.lean
theorem det_to_matrix_orthonormalBasis_of_opposite_orientation
    (h : e.toBasis.orientation ≠ f.toBasis.orientation) : e.toBasis.det f = -1

Proof state:
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
ι : Type u_2
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
e f : OrthonormalBasis ι ℝ E
h : e.toBasis.orientation ≠ f.toBasis.orientation
⊢ e.toBasis.det ⇑f = -1

Tactic:
contrapose! h

Result:
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
ι : Type u_2
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
e f : OrthonormalBasis ι ℝ E
h : e.toBasis.det ⇑f ≠ -1
⊢ e.toBasis.orientation = f.toBasis.orientation

Proof state:
E : Type u_1
inst✝³ : NormedAddCommGroup E
inst✝² : InnerProductSpace ℝ E
ι : Type u_2
inst✝¹ : Fintype ι
inst✝ : DecidableEq ι
e f : OrthonormalBasis ι ℝ E
h : e.toBasis.det ⇑f ≠ -1
⊢ e.toBasis.orientation = f.toBasis.orientation

Tactic:
simp [e.toBasis.orientation_eq_iff_det_pos,
  (e.det_to_matrix_orthonormalBasis_real f).resolve_right h]

Result:
no goals
-- Mathlib/Data/Fin/Tuple/Basic.lean
theorem cons_succ : cons x p i.succ = p i

Proof state:
n : ℕ
α : Fin (n + 1) → Sort u
x : α 0
p : (i : Fin n) → α i.succ
i : Fin n
⊢ cons x p i.succ = p i

Tactic:
simp [cons]

Result:
no goals
-- Mathlib/Data/Matroid/Closure.lean
lemma closure_biUnion_congr (M : Matroid α) (Xs Ys : ι → Set α) (A : Set ι)
    (h : ∀ i ∈ A, M.closure (Xs i) = M.closure (Ys i)) :
    M.closure (⋃ i ∈ A, Xs i) = M.closure (⋃ i ∈ A, Ys i)

Proof state:
ι : Type u_1
α : Type u_2
M : Matroid α
Xs Ys : ι → Set α
A : Set ι
h : ∀ i ∈ A, M.closure (Xs i) = M.closure (Ys i)
⊢ M.closure (⋃ i ∈ A, Xs i) = M.closure (⋃ i ∈ A, Ys i)

Tactic:
rw [← closure_biUnion_closure_eq_closure_biUnion, iUnion₂_congr h,
  closure_biUnion_closure_eq_closure_biUnion]

Result:
no goals
-- Mathlib/RingTheory/DualNumber.lean
@[simp]
lemma isNilpotent_inr (x : M) : IsNilpotent (.inr x : TrivSqZeroExt R M)

Proof state:
R : Type u_1
M : Type u_2
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : SMulCommClass R Rᵐᵒᵖ M
x : M
⊢ inr x ^ 2 = 0

Tactic:
simp [pow_two]

Result:
no goals

Proof state:
R : Type u_1
M : Type u_2
inst✝⁴ : Semiring R
inst✝³ : AddCommMonoid M
inst✝² : Module R M
inst✝¹ : Module Rᵐᵒᵖ M
inst✝ : SMulCommClass R Rᵐᵒᵖ M
x : M
⊢ IsNilpotent (inr x)

Tactic:
refine ⟨2, by simp [pow_two]⟩

Result:
no goals
-- Mathlib/Algebra/Order/Floor.lean
theorem preimage_Icc {a b : α} : ((↑) : ℤ → α) ⁻¹' Set.Icc a b = Set.Icc ⌈a⌉ ⌊b⌋

Proof state:
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
a b : α
⊢ Int.cast ⁻¹' Icc a b = Icc ⌈a⌉ ⌊b⌋

Tactic:
ext

Result:
case h
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
a b : α
x✝ : ℤ
⊢ x✝ ∈ Int.cast ⁻¹' Icc a b ↔ x✝ ∈ Icc ⌈a⌉ ⌊b⌋

Proof state:
case h
α : Type u_2
inst✝¹ : LinearOrderedRing α
inst✝ : FloorRing α
a b : α
x✝ : ℤ
⊢ x✝ ∈ Int.cast ⁻¹' Icc a b ↔ x✝ ∈ Icc ⌈a⌉ ⌊b⌋

Tactic:
simp [ceil_le, le_floor]

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Matching.lean
theorem IsMatching.toEdge.surjective (h : M.IsMatching) : Surjective h.toEdge

Proof state:
V : Type u_1
G : SimpleGraph V
M : G.Subgraph
h : M.IsMatching
⊢ Surjective h.toEdge

Tactic:
rintro ⟨⟨x, y⟩, he⟩

Result:
case mk.mk.mk
V : Type u_1
G : SimpleGraph V
M : G.Subgraph
h : M.IsMatching
val✝ : Sym2 V
x y : V
he : Quot.mk (Sym2.Rel V) (x, y) ∈ M.edgeSet
⊢ ∃ a, h.toEdge a = ⟨Quot.mk (Sym2.Rel V) (x, y), he⟩

Proof state:
case mk.mk.mk
V : Type u_1
G : SimpleGraph V
M : G.Subgraph
h : M.IsMatching
val✝ : Sym2 V
x y : V
he : Quot.mk (Sym2.Rel V) (x, y) ∈ M.edgeSet
⊢ ∃ a, h.toEdge a = ⟨Quot.mk (Sym2.Rel V) (x, y), he⟩

Tactic:
exact ⟨⟨x, M.edge_vert he⟩, h.toEdge_eq_of_adj _ he⟩

Result:
no goals
-- Mathlib/MeasureTheory/Function/L1Space/Integrable.lean
lemma integrable_toReal_iff {f : α → ℝ≥0∞} (hf : AEMeasurable f μ) (hf_ne_top : ∀ᵐ x ∂μ, f x ≠ ∞) :
    Integrable (fun x ↦ (f x).toReal) μ ↔ ∫⁻ x, f x ∂μ ≠ ∞

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
hf_ne_top : ∀ᵐ (x : α) ∂μ, f x ≠ ⊤
⊢ Integrable (fun x => (f x).toReal) μ ↔ ∫⁻ (x : α), f x ∂μ ≠ ⊤

Tactic:
rw [Integrable, hasFiniteIntegral_toReal_iff hf_ne_top]

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
hf_ne_top : ∀ᵐ (x : α) ∂μ, f x ≠ ⊤
⊢ AEStronglyMeasurable (fun x => (f x).toReal) μ ∧ ∫⁻ (x : α), f x ∂μ ≠ ⊤ ↔ ∫⁻ (x : α), f x ∂μ ≠ ⊤

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
f : α → ℝ≥0∞
hf : AEMeasurable f μ
hf_ne_top : ∀ᵐ (x : α) ∂μ, f x ≠ ⊤
⊢ AEStronglyMeasurable (fun x => (f x).toReal) μ ∧ ∫⁻ (x : α), f x ∂μ ≠ ⊤ ↔ ∫⁻ (x : α), f x ∂μ ≠ ⊤

Tactic:
simp only [hf.ennreal_toReal.aestronglyMeasurable, ne_eq, true_and]

Result:
no goals
-- Mathlib/Algebra/Homology/HomologicalComplex.lean
theorem kernel_from_eq_kernel [HasKernels V] {i j : ι} (r : c.Rel i j) :
    kernelSubobject (C.dFrom i) = kernelSubobject (C.d i j)

Proof state:
ι : Type u_1
V : Type u
inst✝² : Category.{v, u} V
inst✝¹ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
inst✝ : HasKernels V
i j : ι
r : c.Rel i j
⊢ kernelSubobject (C.dFrom i) = kernelSubobject (C.d i j)

Tactic:
rw [C.dFrom_eq r]

Result:
ι : Type u_1
V : Type u
inst✝² : Category.{v, u} V
inst✝¹ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
inst✝ : HasKernels V
i j : ι
r : c.Rel i j
⊢ kernelSubobject (C.d i j ≫ (C.xNextIso r).inv) = kernelSubobject (C.d i j)

Proof state:
ι : Type u_1
V : Type u
inst✝² : Category.{v, u} V
inst✝¹ : HasZeroMorphisms V
c : ComplexShape ι
C : HomologicalComplex V c
inst✝ : HasKernels V
i j : ι
r : c.Rel i j
⊢ kernelSubobject (C.d i j ≫ (C.xNextIso r).inv) = kernelSubobject (C.d i j)

Tactic:
apply kernelSubobject_comp_mono

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Unoriented/Basic.lean
theorem sin_eq_zero_iff_angle_eq_zero_or_angle_eq_pi :
    sin (angle x y) = 0 ↔ angle x y = 0 ∨ angle x y = π

Proof state:
V : Type u_1
inst✝¹ : NormedAddCommGroup V
inst✝ : InnerProductSpace ℝ V
x y : V
⊢ sin (angle x y) = 0 ↔ angle x y = 0 ∨ angle x y = π

Tactic:
rw [sin_eq_zero_iff_cos_eq, cos_eq_one_iff_angle_eq_zero, cos_eq_neg_one_iff_angle_eq_pi]

Result:
no goals
-- Mathlib/Data/Vector/MapLemmas.lean
theorem mapAccumr₂_comm (f : α → α → σ → σ × γ) (comm : ∀ a₁ a₂ s, f a₁ a₂ s = f a₂ a₁ s) :
    mapAccumr₂ f xs ys s = mapAccumr₂ f ys xs s

Proof state:
α : Type u_1
γ : Type u_3
σ : Type u_5
n : ℕ
s : σ
xs ys : Vector α n
f : α → α → σ → σ × γ
comm : ∀ (a₁ a₂ : α) (s : σ), f a₁ a₂ s = f a₂ a₁ s
⊢ mapAccumr₂ f xs ys s = mapAccumr₂ f ys xs s

Tactic:
induction xs, ys using Vector.inductionOn₂ generalizing s <;> simp_all

Result:
no goals
-- Mathlib/Order/CompleteLattice.lean
theorem isGLB_biInf {s : Set β} {f : β → α} : IsGLB (f '' s) (⨅ x ∈ s, f x)

Proof state:
α : Type u_1
β : Type u_2
inst✝ : CompleteLattice α
s : Set β
f : β → α
⊢ IsGLB (f '' s) (⨅ x ∈ s, f x)

Tactic:
simpa only [range_comp, Subtype.range_coe, iInf_subtype'] using
  @isGLB_iInf α s _ (f ∘ fun x => (x : β))

Result:
no goals
-- Mathlib/GroupTheory/OreLocalization/Basic.lean
theorem one_div_mul {r : R} {s t : S} : (1 /ₒ t) * (r /ₒ s) = r /ₒ (s * t)

Proof state:
R : Type u_1
inst✝¹ : Monoid R
S : Submonoid R
inst✝ : OreSet S
r : R
s t : ↥S
⊢ ↑s * 1 = 1 * ↑s

Tactic:
simp

Result:
no goals

Proof state:
R : Type u_1
inst✝¹ : Monoid R
S : Submonoid R
inst✝ : OreSet S
r : R
s t : ↥S
⊢ 1 /ₒ t * (r /ₒ s) = r /ₒ (s * t)

Tactic:
simp [oreDiv_mul_char 1 r t s 1 s (by simp)]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Int/Order.lean
theorem mul_pos_of_neg_of_neg {a b : Int} (ha : a < 0) (hb : b < 0) : 0 < a * b

Proof state:
a b : Int
ha : a < 0
hb : b < 0
this : 0 * b < a * b
⊢ 0 < a * b

Tactic:
rwa [Int.zero_mul] at this

Result:
no goals

Proof state:
a b : Int
ha : a < 0
hb : b < 0
⊢ 0 < a * b

Tactic:
have : 0 * b < a * b := Int.mul_lt_mul_of_neg_right ha hb

Result:
a b : Int
ha : a < 0
hb : b < 0
this : 0 * b < a * b
⊢ 0 < a * b
-- Mathlib/CategoryTheory/Limits/Shapes/WideEqualizers.lean
theorem Trident.ofCone_π {F : WalkingParallelFamily J ⥤ C} (t : Cone F) (j) :
    (Trident.ofCone t).π.app j = t.π.app j ≫ eqToHom (by cases j <;> aesop_cat) :=
  rfl

Proof state:
J : Type w
C : Type u
inst✝ : Category.{v, u} C
X Y : C
f : J → (X ⟶ Y)
F : WalkingParallelFamily J ⥤ C
t : Cone F
j : WalkingParallelFamily J
⊢ F.obj j = (parallelFamily fun j => F.map (line j)).obj j

Tactic:
cases j <;> aesop_cat

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Path.lean
lemma eq_of_common_vertex {v : V} {c c' : ConnectedComponent G} (hc : v ∈ c.supp)
    (hc' : v ∈ c'.supp) : c = c'

Proof state:
V : Type u
G : SimpleGraph V
v : V
c c' : G.ConnectedComponent
hc : v ∈ c.supp
hc' : v ∈ c'.supp
⊢ c = c'

Tactic:
simp only [mem_supp_iff] at *

Result:
V : Type u
G : SimpleGraph V
v : V
c c' : G.ConnectedComponent
hc : G.connectedComponentMk v = c
hc' : G.connectedComponentMk v = c'
⊢ c = c'

Proof state:
V : Type u
G : SimpleGraph V
v : V
c c' : G.ConnectedComponent
hc : G.connectedComponentMk v = c
hc' : G.connectedComponentMk v = c'
⊢ c = c'

Tactic:
subst hc hc'

Result:
V : Type u
G : SimpleGraph V
v : V
⊢ G.connectedComponentMk v = G.connectedComponentMk v

Proof state:
V : Type u
G : SimpleGraph V
v : V
⊢ G.connectedComponentMk v = G.connectedComponentMk v

Tactic:
rfl

Result:
no goals
-- Mathlib/Topology/CompactOpen.lean
theorem continuous_precomp (f : C(X, Y)) : Continuous (fun g => g.comp f : C(Y, Z) → C(X, Z)) :=
  continuous_compactOpen.2 fun K hK U hU ↦ by
    simpa only [mapsTo_image_iff] using isOpen_setOf_mapsTo (hK.image f.2) hU

Proof state:
X : Type u_2
Y : Type u_3
Z : Type u_4
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace Z
f : C(X, Y)
K : Set X
hK : IsCompact K
U : Set Z
hU : IsOpen U
⊢ IsOpen {x | MapsTo (⇑(x.comp f)) K U}

Tactic:
simpa only [mapsTo_image_iff] using isOpen_setOf_mapsTo (hK.image f.2) hU

Result:
no goals
-- Mathlib/Algebra/Module/LocalizedModule/Basic.lean
theorem mk'_add_mk' (m₁ m₂ : M) (s₁ s₂ : S) :
    mk' f m₁ s₁ + mk' f m₂ s₂ = mk' f (s₂ • m₁ + s₁ • m₂) (s₁ * s₂)

Proof state:
R : Type u_1
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M'
inst✝² : Module R M
inst✝¹ : Module R M'
f : M →ₗ[R] M'
inst✝ : IsLocalizedModule S f
m₁ m₂ : M
s₁ s₂ : ↥S
⊢ mk' f m₁ s₁ + mk' f m₂ s₂ = mk' f (s₂ • m₁ + s₁ • m₂) (s₁ * s₂)

Tactic:
delta mk'

Result:
R : Type u_1
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M'
inst✝² : Module R M
inst✝¹ : Module R M'
f : M →ₗ[R] M'
inst✝ : IsLocalizedModule S f
m₁ m₂ : M
s₁ s₂ : ↥S
⊢ (fromLocalizedModule S f) (LocalizedModule.mk m₁ s₁) + (fromLocalizedModule S f) (LocalizedModule.mk m₂ s₂) =
    (fromLocalizedModule S f) (LocalizedModule.mk (s₂ • m₁ + s₁ • m₂) (s₁ * s₂))

Proof state:
R : Type u_1
inst✝⁵ : CommSemiring R
S : Submonoid R
M : Type u_2
M' : Type u_3
inst✝⁴ : AddCommMonoid M
inst✝³ : AddCommMonoid M'
inst✝² : Module R M
inst✝¹ : Module R M'
f : M →ₗ[R] M'
inst✝ : IsLocalizedModule S f
m₁ m₂ : M
s₁ s₂ : ↥S
⊢ (fromLocalizedModule S f) (LocalizedModule.mk m₁ s₁) + (fromLocalizedModule S f) (LocalizedModule.mk m₂ s₂) =
    (fromLocalizedModule S f) (LocalizedModule.mk (s₂ • m₁ + s₁ • m₂) (s₁ * s₂))

Tactic:
rw [← map_add, LocalizedModule.mk_add_mk]

Result:
no goals
-- Mathlib/Algebra/Homology/ShortComplex/Preadditive.lean
@[simp]
lemma homologyMap'_nullHomotopic
    (H₁ : S₁.HomologyData) (H₂ : S₂.HomologyData)
    (h₀ : S₁.X₁ ⟶ S₂.X₁) (h₀_f : h₀ ≫ S₂.f = 0)
    (h₁ : S₁.X₂ ⟶ S₂.X₁) (h₂ : S₁.X₃ ⟶ S₂.X₂) (h₃ : S₁.X₃ ⟶ S₂.X₃) (g_h₃ : S₁.g ≫ h₃ = 0) :
    homologyMap' (nullHomotopic _ _ h₀ h₀_f h₁ h₂ h₃ g_h₃) H₁ H₂ = 0

Proof state:
C : Type u_1
inst✝¹ : Category.{u_2, u_1} C
inst✝ : Preadditive C
S₁ S₂ : ShortComplex C
H₁ : S₁.HomologyData
H₂ : S₂.HomologyData
h₀ : S₁.X₁ ⟶ S₂.X₁
h₀_f : h₀ ≫ S₂.f = 0
h₁ : S₁.X₂ ⟶ S₂.X₁
h₂ : S₁.X₃ ⟶ S₂.X₂
h₃ : S₁.X₃ ⟶ S₂.X₃
g_h₃ : S₁.g ≫ h₃ = 0
⊢ homologyMap' (S₁.nullHomotopic S₂ h₀ h₀_f h₁ h₂ h₃ g_h₃) H₁ H₂ = 0

Tactic:
apply leftHomologyMap'_nullHomotopic

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Projective.lean
private lemma nonsingular_add_of_Z_ne_zero {P Q : Fin 3 → F} (hP : W.Nonsingular P)
    (hQ : W.Nonsingular Q) (hPz : P z ≠ 0) (hQz : Q z ≠ 0)
    (hxy : ¬(P x * Q z = Q x * P z ∧ P y * Q z = W.negY Q * P z)) : W.Nonsingular
      ![W.toAffine.addX (P x / P z) (Q x / Q z)
          (W.toAffine.slope (P x / P z) (Q x / Q z) (P y / P z) (Q y / Q z)),
        W.toAffine.addY (P x / P z) (Q x / Q z) (P y / P z)
          (W.toAffine.slope (P x / P z) (Q x / Q z) (P y / P z) (Q y / Q z)), 1] :=
  (nonsingular_some ..).mpr <| Affine.nonsingular_add ((nonsingular_of_Z_ne_zero hPz).mp hP)
    ((nonsingular_of_Z_ne_zero hQz).mp hQ) <| by rwa [← X_eq_iff hPz hQz, ← Y_eq_iff' hPz hQz]

Proof state:
F : Type u
inst✝ : Field F
W : Projective F
P Q : Fin 3 → F
hP : W.Nonsingular P
hQ : W.Nonsingular Q
hPz : P z ≠ 0
hQz : Q z ≠ 0
hxy : ¬(P x * Q z = Q x * P z ∧ P y * Q z = W.negY Q * P z)
⊢ ¬(P x / P z = Q x / Q z ∧ P y / P z = (toAffine W).negY (Q x / Q z) (Q y / Q z))

Tactic:
rwa [← X_eq_iff hPz hQz, ← Y_eq_iff' hPz hQz]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/TakeDrop.lean
theorem takeWhile_cons_of_neg {p : α → Bool} {a : α} {l : List α} (h : ¬ p a) :
    (a :: l).takeWhile p = []

Proof state:
α : Type u_1
p : α → Bool
a : α
l : List α
h : ¬p a = true
⊢ takeWhile p (a :: l) = []

Tactic:
simp [takeWhile_cons, h]

Result:
no goals
-- Mathlib/Algebra/Order/Antidiag/Prod.lean
theorem swap_mem_antidiagonal [AddCommMonoid A] [HasAntidiagonal A] {n : A} {xy : A × A} :
    xy.swap ∈ antidiagonal n ↔ xy ∈ antidiagonal n

Proof state:
A : Type u_1
inst✝¹ : AddCommMonoid A
inst✝ : HasAntidiagonal A
n : A
xy : A × A
⊢ xy.swap ∈ antidiagonal n ↔ xy ∈ antidiagonal n

Tactic:
simp [add_comm]

Result:
no goals