harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Tactic/CongrExclamation.lean
theorem implies_congr' {α α' : Sort u} {β β' : Sort v} (h : α = α') (h' : α' → β = β') :
    (α → β) = (α' → β')

Proof state:
α α' : Sort u
β β' : Sort v
h : α = α'
h' : α' → β = β'
⊢ (α → β) = (α' → β')

Tactic:
cases h

Result:
case refl
α : Sort u
β β' : Sort v
h' : α → β = β'
⊢ (α → β) = (α → β')

Proof state:
case refl
α : Sort u
β β' : Sort v
h' : α → β = β'
⊢ (α → β) = (α → β')

Tactic:
show (∀ (x : α), (fun _ => β) x) = _

Result:
case refl
α : Sort u
β β' : Sort v
h' : α → β = β'
⊢ ((x : α) → (fun x => β) x) = (α → β')

Proof state:
case refl
α : Sort u
β β' : Sort v
h' : α → β = β'
⊢ ((x : α) → (fun x => β) x) = (α → β')

Tactic:
rw [funext h']

Result:
no goals
-- Mathlib/ModelTheory/FinitelyGenerated.lean
theorem FG.cg {N : L.Substructure M} (h : N.FG) : N.CG

Proof state:
case intro.intro
L : Language
M : Type u_1
inst✝ : L.Structure M
s : Set M
hf : s.Finite
h : ((closure L).toFun s).FG
⊢ ((closure L).toFun s).CG

Tactic:
exact ⟨s, hf.countable, rfl⟩

Result:
no goals

Proof state:
L : Language
M : Type u_1
inst✝ : L.Structure M
N : L.Substructure M
h : N.FG
⊢ N.CG

Tactic:
obtain ⟨s, hf, rfl⟩ := fg_def.1 h

Result:
case intro.intro
L : Language
M : Type u_1
inst✝ : L.Structure M
s : Set M
hf : s.Finite
h : ((closure L).toFun s).FG
⊢ ((closure L).toFun s).CG
-- Mathlib/Algebra/Ring/Ext.lean
theorem toNonUnitalNonAssocring_injective :
    Function.Injective (@toNonUnitalNonAssocRing R)

Proof state:
R : Type u
a₁✝ a₂✝ : NonAssocRing R
a✝ : toNonUnitalNonAssocRing = toNonUnitalNonAssocRing
⊢ a₁✝ = a₂✝

Tactic:
ext <;> congr

Result:
no goals

Proof state:
R : Type u
⊢ Function.Injective (@toNonUnitalNonAssocRing R)

Tactic:
intro _ _ _

Result:
R : Type u
a₁✝ a₂✝ : NonAssocRing R
a✝ : toNonUnitalNonAssocRing = toNonUnitalNonAssocRing
⊢ a₁✝ = a₂✝
-- Mathlib/Algebra/Polynomial/Derivative.lean
theorem iterate_derivative_eq_factorial_smul_sum (p : R[X]) (k : ℕ) :
    derivative^[k] p = k ! •
      ∑ x ∈ (derivative^[k] p).support, C ((x + k).choose k • p.coeff (x + k)) * X ^ x

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
k i : ℕ
x✝ : i ∈ ((⇑derivative)^[k] p).support
⊢ C ((i + k).descFactorial k • p.coeff (i + k)) * X ^ i = k ! • (C ((i + k).choose k • p.coeff (i + k)) * X ^ i)

Tactic:
rw [← smul_mul_assoc, smul_C, smul_smul, Nat.descFactorial_eq_factorial_mul_choose]

Result:
no goals

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
k : ℕ
⊢ ∑ x ∈ ((⇑derivative)^[k] p).support, C ((x + k).descFactorial k • p.coeff (x + k)) * X ^ x =
    k ! • ∑ x ∈ ((⇑derivative)^[k] p).support, C ((x + k).choose k • p.coeff (x + k)) * X ^ x

Tactic:
rw [smul_sum]

Result:
R : Type u
inst✝ : Semiring R
p : R[X]
k : ℕ
⊢ ∑ x ∈ ((⇑derivative)^[k] p).support, C ((x + k).descFactorial k • p.coeff (x + k)) * X ^ x =
    ∑ x ∈ ((⇑derivative)^[k] p).support, k ! • (C ((x + k).choose k • p.coeff (x + k)) * X ^ x)

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
k : ℕ
⊢ ∑ x ∈ ((⇑derivative)^[k] p).support, C ((x + k).descFactorial k • p.coeff (x + k)) * X ^ x =
    ∑ x ∈ ((⇑derivative)^[k] p).support, k ! • (C ((x + k).choose k • p.coeff (x + k)) * X ^ x)

Tactic:
refine sum_congr rfl fun i _ ↦ ?_

Result:
R : Type u
inst✝ : Semiring R
p : R[X]
k i : ℕ
x✝ : i ∈ ((⇑derivative)^[k] p).support
⊢ C ((i + k).descFactorial k • p.coeff (i + k)) * X ^ i = k ! • (C ((i + k).choose k • p.coeff (i + k)) * X ^ i)

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
k : ℕ
⊢ (⇑derivative)^[k] p = k ! • ∑ x ∈ ((⇑derivative)^[k] p).support, C ((x + k).choose k • p.coeff (x + k)) * X ^ x

Tactic:
conv_lhs => rw [iterate_derivative_eq_sum]

Result:
R : Type u
inst✝ : Semiring R
p : R[X]
k : ℕ
⊢ ∑ x ∈ ((⇑derivative)^[k] p).support, C ((x + k).descFactorial k • p.coeff (x + k)) * X ^ x =
    k ! • ∑ x ∈ ((⇑derivative)^[k] p).support, C ((x + k).choose k • p.coeff (x + k)) * X ^ x
-- Mathlib/Data/BitVec.lean
lemma toFin_natCast (n : ℕ) : toFin (n : BitVec w) = n

Proof state:
w n : ℕ
⊢ (↑n).toFin = ↑n

Tactic:
rfl

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Connectivity/WalkCounting.lean
theorem coe_finsetWalkLengthLT_eq (n : ℕ) (u v : V) :
    (G.finsetWalkLengthLT n u v : Set (G.Walk u v)) = {p : G.Walk u v | p.length < n}

Proof state:
V : Type u
G : SimpleGraph V
inst✝¹ : DecidableEq V
inst✝ : G.LocallyFinite
n : ℕ
u v : V
⊢ ↑(G.finsetWalkLengthLT n u v) = {p | p.length < n}

Tactic:
ext p

Result:
case h
V : Type u
G : SimpleGraph V
inst✝¹ : DecidableEq V
inst✝ : G.LocallyFinite
n : ℕ
u v : V
p : G.Walk u v
⊢ p ∈ ↑(G.finsetWalkLengthLT n u v) ↔ p ∈ {p | p.length < n}

Proof state:
case h
V : Type u
G : SimpleGraph V
inst✝¹ : DecidableEq V
inst✝ : G.LocallyFinite
n : ℕ
u v : V
p : G.Walk u v
⊢ p ∈ ↑(G.finsetWalkLengthLT n u v) ↔ p ∈ {p | p.length < n}

Tactic:
simp [finsetWalkLengthLT, mem_coe, mem_disjiUnion, mem_finsetWalkLength_iff]

Result:
no goals
-- Mathlib/Topology/Bornology/Absorbs.lean
@[simp]
lemma absorbs_zero_iff [NeBot (cobounded G₀)]
    {E : Type*} [AddMonoid E] [DistribMulAction G₀ E] {s : Set E} :
    Absorbs G₀ s 0 ↔ 0 ∈ s

Proof state:
G₀ : Type u_1
inst✝⁴ : GroupWithZero G₀
inst✝³ : Bornology G₀
inst✝² : (cobounded G₀).NeBot
E : Type u_3
inst✝¹ : AddMonoid E
inst✝ : DistribMulAction G₀ E
s : Set E
⊢ Absorbs G₀ s 0 ↔ 0 ∈ s

Tactic:
simp only [absorbs_iff_eventually_cobounded_mapsTo, ← singleton_zero,
  mapsTo_singleton, smul_zero, eventually_const]

Result:
no goals
-- Mathlib/Algebra/Order/Hom/Monoid.lean
theorem toOrderHom_injective : Injective (toOrderHom : _ → α →o β) := fun f g h =>
  ext <| by convert DFunLike.ext_iff.1 h using 0

Proof state:
α : Type u_2
β : Type u_3
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : MulOneClass α
inst✝ : MulOneClass β
f g : α →*o β
h : f.toOrderHom = g.toOrderHom
⊢ ∀ (a : α), f a = g a

Tactic:
convert DFunLike.ext_iff.1 h using 0

Result:
no goals
-- Mathlib/Data/Set/Finite/Lattice.lean
lemma toFinset_iUnion [Fintype β] [DecidableEq α] (f : β → Set α)
    [∀ w, Fintype (f w)] :
    Set.toFinset (⋃ (x : β), f x) =
    Finset.biUnion (Finset.univ : Finset β) (fun x => (f x).toFinset)

Proof state:
case h
α : Type u
β : Type v
inst✝² : Fintype β
inst✝¹ : DecidableEq α
f : β → Set α
inst✝ : (w : β) → Fintype ↑(f w)
v : α
⊢ v ∈ (⋃ x, f x).toFinset ↔ v ∈ Finset.univ.biUnion fun x => (f x).toFinset

Tactic:
simp only [mem_toFinset, mem_iUnion, Finset.mem_biUnion, Finset.mem_univ, true_and]

Result:
no goals

Proof state:
α : Type u
β : Type v
inst✝² : Fintype β
inst✝¹ : DecidableEq α
f : β → Set α
inst✝ : (w : β) → Fintype ↑(f w)
⊢ (⋃ x, f x).toFinset = Finset.univ.biUnion fun x => (f x).toFinset

Tactic:
ext v

Result:
case h
α : Type u
β : Type v
inst✝² : Fintype β
inst✝¹ : DecidableEq α
f : β → Set α
inst✝ : (w : β) → Fintype ↑(f w)
v : α
⊢ v ∈ (⋃ x, f x).toFinset ↔ v ∈ Finset.univ.biUnion fun x => (f x).toFinset
-- Mathlib/Data/Seq/WSeq.lean
theorem mem_think (s : WSeq α) (a) : a ∈ think s ↔ a ∈ s

Proof state:
case mk.mp
α : Type u
a : α
f : Stream' (Option (Option α))
al : f.IsSeq
h : some (some a) ∈ some none :: f
⊢ ¬some (some a) = some none

Tactic:
intro

Result:
case mk.mp
α : Type u
a : α
f : Stream' (Option (Option α))
al : f.IsSeq
h : some (some a) ∈ some none :: f
a✝ : some (some a) = some none
⊢ False

Proof state:
case mk
α : Type u
a : α
f : Stream' (Option (Option α))
al : f.IsSeq
⊢ a ∈ think ⟨f, al⟩ ↔ a ∈ ⟨f, al⟩

Tactic:
change (some (some a) ∈ some none::f) ↔ some (some a) ∈ f

Result:
case mk
α : Type u
a : α
f : Stream' (Option (Option α))
al : f.IsSeq
⊢ some (some a) ∈ some none :: f ↔ some (some a) ∈ f

Proof state:
case mk.mp
α : Type u
a : α
f : Stream' (Option (Option α))
al : f.IsSeq
h : some (some a) ∈ some none :: f
⊢ some (some a) ∈ f

Tactic:
apply (Stream'.eq_or_mem_of_mem_cons h).resolve_left

Result:
case mk.mp
α : Type u
a : α
f : Stream' (Option (Option α))
al : f.IsSeq
h : some (some a) ∈ some none :: f
⊢ ¬some (some a) = some none

Proof state:
case mk
α : Type u
a : α
f : Stream' (Option (Option α))
al : f.IsSeq
⊢ some (some a) ∈ some none :: f ↔ some (some a) ∈ f

Tactic:
constructor <;> intro h

Result:
case mk.mp
α : Type u
a : α
f : Stream' (Option (Option α))
al : f.IsSeq
h : some (some a) ∈ some none :: f
⊢ some (some a) ∈ f

case mk.mpr
α : Type u
a : α
f : Stream' (Option (Option α))
al : f.IsSeq
h : some (some a) ∈ f
⊢ some (some a) ∈ some none :: f

Proof state:
case mk.mp
α : Type u
a : α
f : Stream' (Option (Option α))
al : f.IsSeq
h : some (some a) ∈ some none :: f
a✝ : some (some a) = some none
⊢ False

Tactic:
injections

Result:
no goals

Proof state:
case mk.mpr
α : Type u
a : α
f : Stream' (Option (Option α))
al : f.IsSeq
h : some (some a) ∈ f
⊢ some (some a) ∈ some none :: f

Tactic:
apply Stream'.mem_cons_of_mem _ h

Result:
no goals

Proof state:
α : Type u
s : WSeq α
a : α
⊢ a ∈ s.think ↔ a ∈ s

Tactic:
obtain ⟨f, al⟩ := s

Result:
case mk
α : Type u
a : α
f : Stream' (Option (Option α))
al : f.IsSeq
⊢ a ∈ think ⟨f, al⟩ ↔ a ∈ ⟨f, al⟩
-- Mathlib/Analysis/RCLike/Basic.lean
theorem I_im' (z : K) : im (I : K) * im z = im z

Proof state:
K : Type u_1
inst✝ : RCLike K
z : K
⊢ im I * im z = im z

Tactic:
rw [mul_comm, I_im]

Result:
no goals
-- Mathlib/Data/List/Nodup.lean
theorem nodup_flatMap {l₁ : List α} {f : α → List β} :
    Nodup (l₁.flatMap f) ↔
      (∀ x ∈ l₁, Nodup (f x)) ∧ Pairwise (Disjoint on f) l₁

Proof state:
α : Type u
β : Type v
l₁ : List α
f : α → List β
⊢ (flatMap f l₁).Nodup ↔ (∀ x ∈ l₁, (f x).Nodup) ∧ Pairwise (Disjoint on f) l₁

Tactic:
simp only [List.flatMap, nodup_flatten, pairwise_map, and_comm, and_left_comm, mem_map,
  exists_imp, and_imp]

Result:
α : Type u
β : Type v
l₁ : List α
f : α → List β
⊢ (Pairwise (fun a b => (f a).Disjoint (f b)) l₁ ∧ ∀ (l : List β) (x : α), f x = l → x ∈ l₁ → l.Nodup) ↔
    Pairwise (Disjoint on f) l₁ ∧ ∀ x ∈ l₁, (f x).Nodup

Proof state:
α : Type u
β : Type v
l₁ : List α
f : α → List β
⊢ (Pairwise (fun a b => (f a).Disjoint (f b)) l₁ ∧ ∀ (l : List β) (x : α), f x = l → x ∈ l₁ → l.Nodup) ↔
    Pairwise (Disjoint on f) l₁ ∧ ∀ x ∈ l₁, (f x).Nodup

Tactic:
rw [show (∀ (l : List β) (x : α), f x = l → x ∈ l₁ → Nodup l) ↔ ∀ x : α, x ∈ l₁ → Nodup (f x)
    from forall_swap.trans <| forall_congr' fun _ => forall_eq']

Result:
no goals
-- Mathlib/Algebra/Group/Basic.lean
theorem mul_eq_one_iff_eq_inv : a * b = 1 ↔ a = b⁻¹ :=
  ⟨eq_inv_of_mul_eq_one_left, fun h ↦ by rw [h, inv_mul_cancel]⟩

Proof state:
G : Type u_3
inst✝ : Group G
a b : G
h : a = b⁻¹
⊢ a * b = 1

Tactic:
rw [h, inv_mul_cancel]

Result:
no goals
-- Mathlib/Combinatorics/Enumerative/IncidenceAlgebra.lean
@[simp]
lemma one_prod_one [DecidableEq α] [DecidableEq β] :
    (.prod 1 1 : IncidenceAlgebra 𝕜 (α × β)) = 1

Proof state:
𝕜 : Type u_2
α : Type u_5
β : Type u_6
inst✝⁴ : Ring 𝕜
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
⊢ IncidenceAlgebra.prod 1 1 = 1

Tactic:
ext x y

Result:
case h
𝕜 : Type u_2
α : Type u_5
β : Type u_6
inst✝⁴ : Ring 𝕜
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
x y : α × β
a✝ : x ≤ y
⊢ (IncidenceAlgebra.prod 1 1) x y = 1 x y

Proof state:
case h
𝕜 : Type u_2
α : Type u_5
β : Type u_6
inst✝⁴ : Ring 𝕜
inst✝³ : Preorder α
inst✝² : Preorder β
inst✝¹ : DecidableEq α
inst✝ : DecidableEq β
x y : α × β
a✝ : x ≤ y
⊢ (IncidenceAlgebra.prod 1 1) x y = 1 x y

Tactic:
simp [Prod.ext_iff, ← ite_and, and_comm]

Result:
no goals
-- Mathlib/Data/List/Chain.lean
theorem chain_eq_iff_eq_replicate {a : α} {l : List α} :
    Chain (· = ·) a l ↔ l = replicate l.length a :=
  match l with
  | [] => by simp
  | b :: l => by
    rw [chain_cons]
    simp (config := {contextual := true}) [eq_comm, replicate_succ, chain_eq_iff_eq_replicate]

Proof state:
α : Type u
a : α
l : List α
⊢ Chain (fun x1 x2 => x1 = x2) a [] ↔ [] = replicate [].length a

Tactic:
simp

Result:
no goals

Proof state:
α : Type u
a : α
l✝ : List α
b : α
l : List α
⊢ a = b ∧ Chain (fun x1 x2 => x1 = x2) b l ↔ b :: l = replicate (b :: l).length a

Tactic:
simp (config := {contextual := true}) [eq_comm, replicate_succ, chain_eq_iff_eq_replicate]

Result:
no goals

Proof state:
α : Type u
a : α
l✝ : List α
b : α
l : List α
⊢ Chain (fun x1 x2 => x1 = x2) a (b :: l) ↔ b :: l = replicate (b :: l).length a

Tactic:
rw [chain_cons]

Result:
α : Type u
a : α
l✝ : List α
b : α
l : List α
⊢ a = b ∧ Chain (fun x1 x2 => x1 = x2) b l ↔ b :: l = replicate (b :: l).length a
-- Mathlib/CategoryTheory/Shift/CommShift.lean
@[reassoc]
lemma shift_comm (a : A) :
    (F₁.commShiftIso a).hom ≫ whiskerRight τ _ =
      whiskerLeft _ τ ≫ (F₂.commShiftIso a).hom

Proof state:
C : Type u_1
D : Type u_2
inst✝⁷ : Category.{u_7, u_1} C
inst✝⁶ : Category.{u_6, u_2} D
F₁ F₂ : C ⥤ D
τ : F₁ ⟶ F₂
A : Type u_5
inst✝⁵ : AddMonoid A
inst✝⁴ : HasShift C A
inst✝³ : HasShift D A
inst✝² : F₁.CommShift A
inst✝¹ : F₂.CommShift A
inst✝ : CommShift τ A
a : A
⊢ (F₁.commShiftIso a).hom ≫ whiskerRight τ (shiftFunctor D a) =
    whiskerLeft (shiftFunctor C a) τ ≫ (F₂.commShiftIso a).hom

Tactic:
apply CommShift.shift_comm

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Unoriented/Affine.lean
theorem dist_eq_add_dist_iff_angle_eq_pi {p₁ p₂ p₃ : P} (hp₁p₂ : p₁ ≠ p₂) (hp₃p₂ : p₃ ≠ p₂) :
    dist p₁ p₃ = dist p₁ p₂ + dist p₃ p₂ ↔ ∠ p₁ p₂ p₃ = π

Proof state:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
hp₁p₂ : p₁ ≠ p₂
hp₃p₂ : p₃ ≠ p₂
⊢ dist p₁ p₃ = dist p₁ p₂ + dist p₃ p₂ ↔ ∠ p₁ p₂ p₃ = π

Tactic:
rw [dist_eq_norm_vsub V, dist_eq_norm_vsub V, dist_eq_norm_vsub V, ← vsub_sub_vsub_cancel_right]

Result:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
hp₁p₂ : p₁ ≠ p₂
hp₃p₂ : p₃ ≠ p₂
⊢ ‖p₁ -ᵥ ?p₃ - (p₃ -ᵥ ?p₃)‖ = ‖p₁ -ᵥ p₂‖ + ‖p₃ -ᵥ p₂‖ ↔ ∠ p₁ p₂ p₃ = π

case p₃
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
hp₁p₂ : p₁ ≠ p₂
hp₃p₂ : p₃ ≠ p₂
⊢ P

Proof state:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
hp₁p₂ : p₁ ≠ p₂
hp₃p₂ : p₃ ≠ p₂
⊢ ‖p₁ -ᵥ ?p₃ - (p₃ -ᵥ ?p₃)‖ = ‖p₁ -ᵥ p₂‖ + ‖p₃ -ᵥ p₂‖ ↔ ∠ p₁ p₂ p₃ = π

case p₃
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : InnerProductSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
p₁ p₂ p₃ : P
hp₁p₂ : p₁ ≠ p₂
hp₃p₂ : p₃ ≠ p₂
⊢ P

Tactic:
exact
  norm_sub_eq_add_norm_iff_angle_eq_pi (fun he => hp₁p₂ (vsub_eq_zero_iff_eq.1 he)) fun he =>
    hp₃p₂ (vsub_eq_zero_iff_eq.1 he)

Result:
no goals
-- Mathlib/CategoryTheory/ChosenFiniteProducts.lean
@[reassoc (attr := simp)]
lemma lift_δ {X Y Z : C} (f : X ⟶ Y) (g : X ⟶ Z) :
    F.map (lift f g) ≫ OplaxMonoidal.δ F _ _ = lift (F.map f) (F.map g)

Proof state:
C : Type u
inst✝³ : Category.{v, u} C
inst✝² : ChosenFiniteProducts C
D : Type u₁
inst✝¹ : Category.{v₁, u₁} D
inst✝ : ChosenFiniteProducts D
F : C ⥤ D
X Y Z : C
f : X ⟶ Y
g : X ⟶ Z
⊢ F.map (lift f g) ≫ OplaxMonoidal.δ F Y Z = lift (F.map f) (F.map g)

Tactic:
apply hom_ext <;> simp [← F.map_comp]

Result:
no goals
-- Mathlib/RingTheory/Ideal/Maps.lean
theorem map_mul {R} [Semiring R] [FunLike F R S] [RingHomClass F R S] (f : F) (I J : Ideal R) :
    map f (I * J) = map f I * map f J :=
  le_antisymm
    (map_le_iff_le_comap.2 <|
      mul_le.2 fun r hri s hsj =>
        show (f (r * s)) ∈ map f I * map f J by
          rw [_root_.map_mul]; exact mul_mem_mul (mem_map_of_mem f hri) (mem_map_of_mem f hsj))
    (span_mul_span (↑f '' ↑I) (↑f '' ↑J) ▸ (span_le.2 <|
      Set.iUnion₂_subset fun _ ⟨r, hri, hfri⟩ =>
        Set.iUnion₂_subset fun _ ⟨s, hsj, hfsj⟩ =>
          Set.singleton_subset_iff.2 <|
            hfri ▸ hfsj ▸ by rw [← _root_.map_mul]; exact mem_map_of_mem f (mul_mem_mul hri hsj)))

Proof state:
S : Type v
F : Type u_1
inst✝³ : CommSemiring S
R : Type u_2
inst✝² : Semiring R
inst✝¹ : FunLike F R S
inst✝ : RingHomClass F R S
f : F
I J : Ideal R
x✝³ : S
x✝² : x✝³ ∈ ⇑f '' ↑I
r : R
hri : r ∈ ↑I
hfri : f r = x✝³
x✝¹ : S
x✝ : x✝¹ ∈ ⇑f '' ↑J
s : R
hsj : s ∈ ↑J
hfsj : f s = x✝¹
⊢ f (r * s) ∈ ↑(map f (I * J))

Tactic:
exact mem_map_of_mem f (mul_mem_mul hri hsj)

Result:
no goals

Proof state:
S : Type v
F : Type u_1
inst✝³ : CommSemiring S
R : Type u_2
inst✝² : Semiring R
inst✝¹ : FunLike F R S
inst✝ : RingHomClass F R S
f : F
I J : Ideal R
r : R
hri : r ∈ I
s : R
hsj : s ∈ J
⊢ f (r * s) ∈ map f I * map f J

Tactic:
rw [_root_.map_mul]

Result:
S : Type v
F : Type u_1
inst✝³ : CommSemiring S
R : Type u_2
inst✝² : Semiring R
inst✝¹ : FunLike F R S
inst✝ : RingHomClass F R S
f : F
I J : Ideal R
r : R
hri : r ∈ I
s : R
hsj : s ∈ J
⊢ f r * f s ∈ map f I * map f J

Proof state:
S : Type v
F : Type u_1
inst✝³ : CommSemiring S
R : Type u_2
inst✝² : Semiring R
inst✝¹ : FunLike F R S
inst✝ : RingHomClass F R S
f : F
I J : Ideal R
x✝³ : S
x✝² : x✝³ ∈ ⇑f '' ↑I
r : R
hri : r ∈ ↑I
hfri : f r = x✝³
x✝¹ : S
x✝ : x✝¹ ∈ ⇑f '' ↑J
s : R
hsj : s ∈ ↑J
hfsj : f s = x✝¹
⊢ f r * f s ∈ ↑(map f (I * J))

Tactic:
rw [← _root_.map_mul]

Result:
S : Type v
F : Type u_1
inst✝³ : CommSemiring S
R : Type u_2
inst✝² : Semiring R
inst✝¹ : FunLike F R S
inst✝ : RingHomClass F R S
f : F
I J : Ideal R
x✝³ : S
x✝² : x✝³ ∈ ⇑f '' ↑I
r : R
hri : r ∈ ↑I
hfri : f r = x✝³
x✝¹ : S
x✝ : x✝¹ ∈ ⇑f '' ↑J
s : R
hsj : s ∈ ↑J
hfsj : f s = x✝¹
⊢ f (r * s) ∈ ↑(map f (I * J))

Proof state:
S : Type v
F : Type u_1
inst✝³ : CommSemiring S
R : Type u_2
inst✝² : Semiring R
inst✝¹ : FunLike F R S
inst✝ : RingHomClass F R S
f : F
I J : Ideal R
r : R
hri : r ∈ I
s : R
hsj : s ∈ J
⊢ f r * f s ∈ map f I * map f J

Tactic:
exact mul_mem_mul (mem_map_of_mem f hri) (mem_map_of_mem f hsj)

Result:
no goals
-- Mathlib/Algebra/Ring/Periodic.lean
theorem Periodic.nat_mul [Semiring α] (h : Periodic f c) (n : ℕ) : Periodic f (n * c)

Proof state:
α : Type u_1
β : Type u_2
f : α → β
c : α
inst✝ : Semiring α
h : Periodic f c
n : ℕ
⊢ Periodic f (↑n * c)

Tactic:
simpa only [nsmul_eq_mul] using h.nsmul n

Result:
no goals
-- Mathlib/Order/OmegaCompletePartialOrder.lean
@[simp] lemma range_pair (a b : α) (hab) : Set.range (pair a b hab) = {a, b}

Proof state:
α : Type u_2
inst✝ : Preorder α
a b : α
hab : a ≤ b
⊢ Set.range ⇑(pair a b hab) = {a, b}

Tactic:
ext

Result:
case h
α : Type u_2
inst✝ : Preorder α
a b : α
hab : a ≤ b
x✝ : α
⊢ x✝ ∈ Set.range ⇑(pair a b hab) ↔ x✝ ∈ {a, b}

Proof state:
case h
α : Type u_2
inst✝ : Preorder α
a b : α
hab : a ≤ b
x✝ : α
⊢ x✝ ∈ Set.range ⇑(pair a b hab) ↔ x✝ ∈ {a, b}

Tactic:
exact Nat.or_exists_add_one.symm.trans (by aesop)

Result:
no goals

Proof state:
α : Type u_2
inst✝ : Preorder α
a b : α
hab : a ≤ b
x✝ : α
⊢ ((pair a b hab) 0 = x✝ ∨ ∃ n, (pair a b hab) (n + 1) = x✝) ↔ x✝ ∈ {a, b}

Tactic:
aesop

Result:
no goals
-- Mathlib/Probability/Kernel/MeasurableLIntegral.lean
theorem _root_.Measurable.setLIntegral_kernel_prod_left {f : β → α → ℝ≥0∞}
    (hf : Measurable (uncurry f)) {s : Set β} (hs : MeasurableSet s) :
    Measurable fun b => ∫⁻ a in s, f a b ∂κ b

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
f : β → α → ℝ≥0∞
hf : Measurable (uncurry f)
s : Set β
hs : MeasurableSet s
⊢ Measurable fun b => ∫⁻ (a : β) in s, f a b ∂κ b

Tactic:
simp_rw [← lintegral_restrict κ hs]

Result:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
f : β → α → ℝ≥0∞
hf : Measurable (uncurry f)
s : Set β
hs : MeasurableSet s
⊢ Measurable fun b => ∫⁻ (a : β), f a b ∂(κ.restrict hs) b

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
κ : Kernel α β
inst✝ : IsSFiniteKernel κ
f : β → α → ℝ≥0∞
hf : Measurable (uncurry f)
s : Set β
hs : MeasurableSet s
⊢ Measurable fun b => ∫⁻ (a : β), f a b ∂(κ.restrict hs) b

Tactic:
fun_prop

Result:
no goals
-- Mathlib/AlgebraicTopology/SimplicialSet/StrictSegal.lean
theorem spineToSimplex_vertex (i : Fin (n + 1)) (f : Path X n) :
    X.map (SimplexCategory.const ⦋0⦌ ⦋n⦌ i).op (spineToSimplex f) = f.vertex i

Proof state:
X : SSet
inst✝ : X.StrictSegal
n : ℕ
i : Fin (n + 1)
f : X.Path n
⊢ X.map (⦋0⦌.const ⦋n⦌ i).op (spineToSimplex f) = f.vertex i

Tactic:
rw [← spine_vertex, spine_spineToSimplex]

Result:
no goals
-- Mathlib/Data/Nat/Init.lean
@[simp]
lemma decreasingInduction_succ' {n} {motive : (m : ℕ) → m ≤ n + 1 → Sort*} (of_succ self) :
    decreasingInduction (motive := motive) of_succ self n.le_succ = of_succ _ _ self

Proof state:
n : ℕ
motive : (m : ℕ) → m ≤ n + 1 → Sort u_1
of_succ : (k : ℕ) → (h : k < n + 1) → motive (k + 1) h → motive k ⋯
self : motive (n + 1) ⋯
⊢ leRec (motive := fun {n_1} mn =>
      {motive : (m : ℕ) → m ≤ n_1 → Sort u_1} →
        ((k : ℕ) → (h : k < n_1) → motive (k + 1) h → motive k ⋯) → motive n_1 ⋯ → motive n mn)
      (fun {motive} of_succ self => self)
      (fun ⦃k⦄ h ih {motive} of_succ self => ih (fun i hi => of_succ i ⋯) (of_succ k ⋯ self)) ⋯ of_succ self =
    of_succ n ⋯ self

Tactic:
rw [leRec_succ']

Result:
no goals

Proof state:
n : ℕ
motive : (m : ℕ) → m ≤ n + 1 → Sort u_1
of_succ : (k : ℕ) → (h : k < n + 1) → motive (k + 1) h → motive k ⋯
self : motive (n + 1) ⋯
⊢ decreasingInduction of_succ self ⋯ = of_succ n ⋯ self

Tactic:
dsimp only [decreasingInduction]

Result:
n : ℕ
motive : (m : ℕ) → m ≤ n + 1 → Sort u_1
of_succ : (k : ℕ) → (h : k < n + 1) → motive (k + 1) h → motive k ⋯
self : motive (n + 1) ⋯
⊢ leRec (motive := fun {n_1} mn =>
      {motive : (m : ℕ) → m ≤ n_1 → Sort u_1} →
        ((k : ℕ) → (h : k < n_1) → motive (k + 1) h → motive k ⋯) → motive n_1 ⋯ → motive n mn)
      (fun {motive} of_succ self => self)
      (fun ⦃k⦄ h ih {motive} of_succ self => ih (fun i hi => of_succ i ⋯) (of_succ k ⋯ self)) ⋯ of_succ self =
    of_succ n ⋯ self
-- Mathlib/Algebra/Polynomial/Reverse.lean
@[simp] lemma reverse_C_add (p : R[X]) (t : R) :
    reverse (C t + p) = C t * X ^ p.natDegree + reverse p

Proof state:
R : Type u_1
inst✝ : Semiring R
p : R[X]
t : R
⊢ (C t + p).reverse = C t * X ^ p.natDegree + p.reverse

Tactic:
rw [add_comm, reverse_add_C, add_comm]

Result:
no goals