harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/MeasureTheory/Group/Prod.lean
theorem quasiMeasurePreserving_div_left [IsMulLeftInvariant μ] (g : G) :
    QuasiMeasurePreserving (fun h : G => g / h) μ μ

Proof state:
G : Type u_1
inst✝⁵ : MeasurableSpace G
inst✝⁴ : Group G
inst✝³ : MeasurableMul₂ G
μ : Measure G
inst✝² : SFinite μ
inst✝¹ : MeasurableInv G
inst✝ : μ.IsMulLeftInvariant
g : G
⊢ QuasiMeasurePreserving (fun h => g * h⁻¹) μ μ

Tactic:
exact
  (measurePreserving_mul_left μ g).quasiMeasurePreserving.comp (quasiMeasurePreserving_inv μ)

Result:
no goals

Proof state:
G : Type u_1
inst✝⁵ : MeasurableSpace G
inst✝⁴ : Group G
inst✝³ : MeasurableMul₂ G
μ : Measure G
inst✝² : SFinite μ
inst✝¹ : MeasurableInv G
inst✝ : μ.IsMulLeftInvariant
g : G
⊢ QuasiMeasurePreserving (fun h => g / h) μ μ

Tactic:
simp_rw [div_eq_mul_inv]

Result:
G : Type u_1
inst✝⁵ : MeasurableSpace G
inst✝⁴ : Group G
inst✝³ : MeasurableMul₂ G
μ : Measure G
inst✝² : SFinite μ
inst✝¹ : MeasurableInv G
inst✝ : μ.IsMulLeftInvariant
g : G
⊢ QuasiMeasurePreserving (fun h => g * h⁻¹) μ μ
-- Mathlib/Algebra/Module/LinearMap/Polynomial.lean
lemma polyCharpoly_baseChange (A : Type*) [CommRing A] [Algebra R A] :
    polyCharpoly (tensorProduct _ _ _ _ ∘ₗ φ.baseChange A) (basis A b) =
      (polyCharpoly φ b).map (MvPolynomial.map (algebraMap R A))

Proof state:
R : Type u_1
L : Type u_2
M : Type u_3
ι : Type u_5
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup L
inst✝⁸ : Module R L
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
φ : L →ₗ[R] End R M
inst✝⁵ : Fintype ι
inst✝⁴ : DecidableEq ι
inst✝³ : Free R M
inst✝² : Module.Finite R M
b : Basis ι R L
A : Type u_8
inst✝¹ : CommRing A
inst✝ : Algebra R A
⊢ (tensorProduct R A M M ∘ₗ baseChange A φ).polyCharpolyAux (basis A b) (Free.chooseBasis A (TensorProduct R A M)) =
    (tensorProduct R A M M ∘ₗ baseChange A φ).polyCharpolyAux (basis A b) (basis A (Free.chooseBasis R M))

Tactic:
apply polyCharpolyAux_basisIndep

Result:
no goals

Proof state:
R : Type u_1
L : Type u_2
M : Type u_3
ι : Type u_5
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup L
inst✝⁸ : Module R L
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
φ : L →ₗ[R] End R M
inst✝⁵ : Fintype ι
inst✝⁴ : DecidableEq ι
inst✝³ : Free R M
inst✝² : Module.Finite R M
b : Basis ι R L
A : Type u_8
inst✝¹ : CommRing A
inst✝ : Algebra R A
⊢ (tensorProduct R A M M ∘ₗ baseChange A φ).polyCharpolyAux (basis A b) (Free.chooseBasis A (TensorProduct R A M)) =
    Polynomial.map (MvPolynomial.map (algebraMap R A)) (φ.polyCharpolyAux b (Free.chooseBasis R M))

Tactic:
rw [← φ.polyCharpolyAux_baseChange]

Result:
R : Type u_1
L : Type u_2
M : Type u_3
ι : Type u_5
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup L
inst✝⁸ : Module R L
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
φ : L →ₗ[R] End R M
inst✝⁵ : Fintype ι
inst✝⁴ : DecidableEq ι
inst✝³ : Free R M
inst✝² : Module.Finite R M
b : Basis ι R L
A : Type u_8
inst✝¹ : CommRing A
inst✝ : Algebra R A
⊢ (tensorProduct R A M M ∘ₗ baseChange A φ).polyCharpolyAux (basis A b) (Free.chooseBasis A (TensorProduct R A M)) =
    (tensorProduct R A M M ∘ₗ baseChange A φ).polyCharpolyAux (basis A b) (basis A (Free.chooseBasis R M))

Proof state:
R : Type u_1
L : Type u_2
M : Type u_3
ι : Type u_5
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup L
inst✝⁸ : Module R L
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
φ : L →ₗ[R] End R M
inst✝⁵ : Fintype ι
inst✝⁴ : DecidableEq ι
inst✝³ : Free R M
inst✝² : Module.Finite R M
b : Basis ι R L
A : Type u_8
inst✝¹ : CommRing A
inst✝ : Algebra R A
⊢ (tensorProduct R A M M ∘ₗ baseChange A φ).polyCharpoly (basis A b) =
    Polynomial.map (MvPolynomial.map (algebraMap R A)) (φ.polyCharpoly b)

Tactic:
unfold polyCharpoly

Result:
R : Type u_1
L : Type u_2
M : Type u_3
ι : Type u_5
inst✝¹⁰ : CommRing R
inst✝⁹ : AddCommGroup L
inst✝⁸ : Module R L
inst✝⁷ : AddCommGroup M
inst✝⁶ : Module R M
φ : L →ₗ[R] End R M
inst✝⁵ : Fintype ι
inst✝⁴ : DecidableEq ι
inst✝³ : Free R M
inst✝² : Module.Finite R M
b : Basis ι R L
A : Type u_8
inst✝¹ : CommRing A
inst✝ : Algebra R A
⊢ (tensorProduct R A M M ∘ₗ baseChange A φ).polyCharpolyAux (basis A b) (Free.chooseBasis A (TensorProduct R A M)) =
    Polynomial.map (MvPolynomial.map (algebraMap R A)) (φ.polyCharpolyAux b (Free.chooseBasis R M))
-- Mathlib/Data/ENNReal/Inv.lean
lemma sSup_mul {a : ℝ≥0∞} : sSup s * a = ⨆ b ∈ s, b * a

Proof state:
s : Set ℝ≥0∞
a : ℝ≥0∞
⊢ sSup s * a = ⨆ b ∈ s, b * a

Tactic:
simp only [sSup_eq_iSup, iSup_mul]

Result:
no goals
-- Mathlib/Algebra/Ring/Subring/Defs.lean
lemma NonUnitalSubring.toSubring_toNonUnitalSubring (S : NonUnitalSubring R) (h1 : (1 : R) ∈ S) :
    (NonUnitalSubring.toSubring S h1).toNonUnitalSubring = S

Proof state:
case mk
R : Type u
inst✝ : Ring R
toNonUnitalSubsemiring✝ : NonUnitalSubsemiring R
neg_mem'✝ : ∀ {x : R}, x ∈ toNonUnitalSubsemiring✝.carrier → -x ∈ toNonUnitalSubsemiring✝.carrier
h1 : 1 ∈ { toNonUnitalSubsemiring := toNonUnitalSubsemiring✝, neg_mem' := neg_mem'✝ }
⊢ ({ toNonUnitalSubsemiring := toNonUnitalSubsemiring✝, neg_mem' := neg_mem'✝ }.toSubring h1).toNonUnitalSubring =
    { toNonUnitalSubsemiring := toNonUnitalSubsemiring✝, neg_mem' := neg_mem'✝ }

Tactic:
rfl

Result:
no goals

Proof state:
R : Type u
inst✝ : Ring R
S : NonUnitalSubring R
h1 : 1 ∈ S
⊢ (S.toSubring h1).toNonUnitalSubring = S

Tactic:
cases S

Result:
case mk
R : Type u
inst✝ : Ring R
toNonUnitalSubsemiring✝ : NonUnitalSubsemiring R
neg_mem'✝ : ∀ {x : R}, x ∈ toNonUnitalSubsemiring✝.carrier → -x ∈ toNonUnitalSubsemiring✝.carrier
h1 : 1 ∈ { toNonUnitalSubsemiring := toNonUnitalSubsemiring✝, neg_mem' := neg_mem'✝ }
⊢ ({ toNonUnitalSubsemiring := toNonUnitalSubsemiring✝, neg_mem' := neg_mem'✝ }.toSubring h1).toNonUnitalSubring =
    { toNonUnitalSubsemiring := toNonUnitalSubsemiring✝, neg_mem' := neg_mem'✝ }
-- Mathlib/Topology/UniformSpace/Equicontinuity.lean
theorem equicontinuousOn_iInf_rng {u : κ → UniformSpace α'} {F : ι → X → α'}
    {S : Set X} :
    EquicontinuousOn (uα := ⨅ k, u k) F S ↔ ∀ k, EquicontinuousOn (uα := u k) F S

Proof state:
ι : Type u_1
κ : Type u_2
X : Type u_3
α' : Type u_7
tX : TopologicalSpace X
u : κ → UniformSpace α'
F : ι → X → α'
S : Set X
⊢ EquicontinuousOn F S ↔ ∀ (k : κ), EquicontinuousOn F S

Tactic:
simp_rw [EquicontinuousOn, equicontinuousWithinAt_iInf_rng, @forall_swap _ κ]

Result:
no goals
-- Mathlib/Data/Set/Lattice.lean
theorem iUnion_of_singleton (α : Type*) : (⋃ x, {x} : Set α) = univ

Proof state:
α : Type u_12
⊢ ⋃ x, {x} = univ

Tactic:
simp [Set.ext_iff]

Result:
no goals
-- Mathlib/GroupTheory/Perm/Cycle/Concrete.lean
theorem toList_formPerm_singleton (x y : α) : toList (formPerm [x]) y = []

Proof state:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
x y : α
⊢ [x].formPerm.toList y = []

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Ring/Subring/Basic.lean
theorem map_range : f.range.map g = (g.comp f).range

Proof state:
R : Type u
S : Type v
T : Type w
inst✝² : Ring R
inst✝¹ : Ring S
inst✝ : Ring T
g : S →+* T
f : R →+* S
⊢ Subring.map g f.range = (g.comp f).range

Tactic:
simpa only [range_eq_map] using (⊤ : Subring R).map_map g f

Result:
no goals
-- Mathlib/Analysis/MellinTransform.lean
theorem hasMellin_cpow_Ioc (a : ℂ) {s : ℂ} (hs : 0 < re s + re a) :
    HasMellin (indicator (Ioc 0 1) (fun t => ↑t ^ a : ℝ → ℂ)) s (1 / (s + a))

Proof state:
a s : ℂ
hs : 0 < s.re + a.re
⊢ HasMellin ((Ioc 0 1).indicator fun t => ↑t ^ a) s (1 / (s + a))

Tactic:
have := hasMellin_one_Ioc (by rwa [add_re] : 0 < (s + a).re)

Result:
a s : ℂ
hs : 0 < s.re + a.re
this : HasMellin ((Ioc 0 1).indicator fun x => 1) (s + a) (1 / (s + a))
⊢ HasMellin ((Ioc 0 1).indicator fun t => ↑t ^ a) s (1 / (s + a))

Proof state:
a s : ℂ
hs : 0 < s.re + a.re
this : HasMellin ((Ioc 0 1).indicator fun x => 1) (s + a) (1 / (s + a))
⊢ HasMellin ((Ioc 0 1).indicator fun t => ↑t ^ a) s (1 / (s + a))

Tactic:
simp_rw [HasMellin, ← MellinConvergent.cpow_smul, ← mellin_cpow_smul, ← indicator_smul,
  smul_eq_mul, mul_one] at this

Result:
a s : ℂ
hs : 0 < s.re + a.re
this :
  MellinConvergent ((Ioc 0 1).indicator fun a_1 => ↑a_1 ^ a) s ∧
    mellin ((Ioc 0 1).indicator fun a_1 => ↑a_1 ^ a) s = 1 / (s + a)
⊢ HasMellin ((Ioc 0 1).indicator fun t => ↑t ^ a) s (1 / (s + a))

Proof state:
a s : ℂ
hs : 0 < s.re + a.re
⊢ 0 < (s + a).re

Tactic:
rwa [add_re]

Result:
no goals

Proof state:
a s : ℂ
hs : 0 < s.re + a.re
this :
  MellinConvergent ((Ioc 0 1).indicator fun a_1 => ↑a_1 ^ a) s ∧
    mellin ((Ioc 0 1).indicator fun a_1 => ↑a_1 ^ a) s = 1 / (s + a)
⊢ HasMellin ((Ioc 0 1).indicator fun t => ↑t ^ a) s (1 / (s + a))

Tactic:
exact this

Result:
no goals
-- Mathlib/Algebra/CubicDiscriminant.lean
theorem degree_of_d_eq_zero (ha : P.a = 0) (hb : P.b = 0) (hc : P.c = 0) (hd : P.d = 0) :
    P.toPoly.degree = ⊥

Proof state:
R : Type u_1
P : Cubic R
inst✝ : Semiring R
ha : P.a = 0
hb : P.b = 0
hc : P.c = 0
hd : P.d = 0
⊢ P.toPoly.degree = ⊥

Tactic:
rw [of_d_eq_zero ha hb hc hd, degree_zero]

Result:
no goals
-- Mathlib/MeasureTheory/MeasurableSpace/Basic.lean
theorem map_const {m} (b : β) : MeasurableSpace.map (fun _a : α ↦ b) m = ⊤ :=
  eq_top_iff.2 <| fun s _ ↦ by rw [map_def]; by_cases h : b ∈ s <;> simp [h]

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
b : β
s : Set β
x✝ : MeasurableSet s
⊢ MeasurableSet ((fun _a => b) ⁻¹' s)

Tactic:
by_cases h : b ∈ s <;> simp [h]

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
b : β
s : Set β
x✝ : MeasurableSet s
⊢ MeasurableSet s

Tactic:
rw [map_def]

Result:
α : Type u_1
β : Type u_2
m : MeasurableSpace α
b : β
s : Set β
x✝ : MeasurableSet s
⊢ MeasurableSet ((fun _a => b) ⁻¹' s)
-- Mathlib/GroupTheory/MonoidLocalization/Basic.lean
theorem mk_prod {ι} (t : Finset ι) (f : ι → M) (s : ι → S) :
    ∏ i ∈ t, mk (f i) (s i) = mk (∏ i ∈ t, f i) (∏ i ∈ t, s i)

Proof state:
M : Type u_1
inst✝ : CommMonoid M
S : Submonoid M
ι : Type u_4
t : Finset ι
f : ι → M
s : ι → ↥S
⊢ ∏ i ∈ t, mk (f i) (s i) = mk (∏ i ∈ t, f i) (∏ i ∈ t, s i)

Tactic:
classical
induction t using Finset.induction_on <;> simp [mk_one, Finset.prod_insert, *, mk_mul]

Result:
no goals

Proof state:
M : Type u_1
inst✝ : CommMonoid M
S : Submonoid M
ι : Type u_4
t : Finset ι
f : ι → M
s : ι → ↥S
⊢ ∏ i ∈ t, mk (f i) (s i) = mk (∏ i ∈ t, f i) (∏ i ∈ t, s i)

Tactic:
induction t using Finset.induction_on <;> simp [mk_one, Finset.prod_insert, *, mk_mul]

Result:
no goals
-- Mathlib/CategoryTheory/Monoidal/Category.lean
theorem hom_inv_whiskerRight' {X Y : C} (f : X ⟶ Y) [IsIso f] (Z : C) :
    f ▷ Z ≫ inv f ▷ Z = 𝟙 (X ⊗ Z)

Proof state:
C : Type u
𝒞 : Category.{v, u} C
inst✝¹ : MonoidalCategory C
X Y : C
f : X ⟶ Y
inst✝ : IsIso f
Z : C
⊢ f ▷ Z ≫ inv f ▷ Z = 𝟙 (X ⊗ Z)

Tactic:
rw [← comp_whiskerRight, IsIso.hom_inv_id, id_whiskerRight]

Result:
no goals
-- Mathlib/Data/ZMod/Basic.lean
theorem natCast_mod (a : ℕ) (n : ℕ) : ((a % n : ℕ) : ZMod n) = a

Proof state:
a n : ℕ
⊢ ↑(a % n) = ↑a

Tactic:
conv =>
    rhs
    rw [← Nat.mod_add_div a n]

Result:
a n : ℕ
⊢ ↑(a % n) = ↑(a % n + n * (a / n))

Proof state:
a n : ℕ
⊢ ↑(a % n) = ↑(a % n + n * (a / n))

Tactic:
simp

Result:
no goals
-- Mathlib/LinearAlgebra/Finsupp/Supported.lean
theorem restrictDom_comp_subtype (s : Set α) [DecidablePred (· ∈ s)] :
    (restrictDom M R s).comp (Submodule.subtype _) = LinearMap.id

Proof state:
case h.a.h
α : Type u_1
M : Type u_2
R : Type u_5
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
s : Set α
inst✝ : DecidablePred fun x => x ∈ s
l : ↥(supported M R s)
a : α
⊢ ↑((restrictDom M R s ∘ₗ (supported M R s).subtype) l) a = ↑(LinearMap.id l) a

Tactic:
by_cases h : a ∈ s

Result:
case pos
α : Type u_1
M : Type u_2
R : Type u_5
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
s : Set α
inst✝ : DecidablePred fun x => x ∈ s
l : ↥(supported M R s)
a : α
h : a ∈ s
⊢ ↑((restrictDom M R s ∘ₗ (supported M R s).subtype) l) a = ↑(LinearMap.id l) a

case neg
α : Type u_1
M : Type u_2
R : Type u_5
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
s : Set α
inst✝ : DecidablePred fun x => x ∈ s
l : ↥(supported M R s)
a : α
h : a ∉ s
⊢ ↑((restrictDom M R s ∘ₗ (supported M R s).subtype) l) a = ↑(LinearMap.id l) a

Proof state:
case pos
α : Type u_1
M : Type u_2
R : Type u_5
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
s : Set α
inst✝ : DecidablePred fun x => x ∈ s
l : ↥(supported M R s)
a : α
h : a ∈ s
⊢ ↑((restrictDom M R s ∘ₗ (supported M R s).subtype) l) a = ↑(LinearMap.id l) a

Tactic:
simp [h]

Result:
no goals

Proof state:
α : Type u_1
M : Type u_2
R : Type u_5
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
s : Set α
inst✝ : DecidablePred fun x => x ∈ s
⊢ restrictDom M R s ∘ₗ (supported M R s).subtype = LinearMap.id

Tactic:
ext l a

Result:
case h.a.h
α : Type u_1
M : Type u_2
R : Type u_5
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
s : Set α
inst✝ : DecidablePred fun x => x ∈ s
l : ↥(supported M R s)
a : α
⊢ ↑((restrictDom M R s ∘ₗ (supported M R s).subtype) l) a = ↑(LinearMap.id l) a

Proof state:
case neg
α : Type u_1
M : Type u_2
R : Type u_5
inst✝³ : Semiring R
inst✝² : AddCommMonoid M
inst✝¹ : Module R M
s : Set α
inst✝ : DecidablePred fun x => x ∈ s
l : ↥(supported M R s)
a : α
h : a ∉ s
⊢ ↑((restrictDom M R s ∘ₗ (supported M R s).subtype) l) a = ↑(LinearMap.id l) a

Tactic:
simpa [h] using ((mem_supported' R l.1).1 l.2 a h).symm

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Std/Sat/AIG/Lemmas.lean
theorem denote_idx_gate {aig : AIG α} {hstart} (h : aig.decls[start] = .gate lhs rhs linv rinv) :
    ⟦aig, ⟨start, hstart⟩, assign⟧
      =
    (
      (⟦aig, ⟨lhs, by have := aig.invariant hstart h; omega⟩, assign⟧ ^^ linv)
        &&
      (⟦aig, ⟨rhs, by have := aig.invariant hstart h; omega⟩, assign⟧ ^^ rinv)
    )

Proof state:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
start : Nat
assign : α → Bool
lhs : Nat
linv : Bool
rhs : Nat
rinv : Bool
aig : AIG α
hstart : start < aig.decls.size
h : aig.decls[start] = Decl.gate lhs rhs linv rinv
⊢ denote.go { aig := aig, ref := { gate := start, hgate := hstart } }.ref.gate
      { aig := aig, ref := { gate := start, hgate := hstart } }.aig.decls assign ⋯ ⋯ =
    ((denote.go { aig := aig, ref := { gate := lhs, hgate := ⋯ } }.ref.gate
          { aig := aig, ref := { gate := lhs, hgate := ⋯ } }.aig.decls assign ⋯ ⋯ ^^
        linv) &&
      (denote.go { aig := aig, ref := { gate := rhs, hgate := ⋯ } }.ref.gate
          { aig := aig, ref := { gate := rhs, hgate := ⋯ } }.aig.decls assign ⋯ ⋯ ^^
        rinv))

Tactic:
conv =>
  lhs
  unfold denote.go

Result:
α : Type
inst✝¹ : Hashable α
inst✝ : DecidableEq α
start : Nat
assign : α → Bool
lhs : Nat
linv : Bool
rhs : Nat
rinv : Bool
aig : AIG α
hstart : start < aig.decls.size
h : aig.decls[start] = Decl.gate lhs rhs linv rinv
⊢ (match elem :
      { aig := aig,
              ref :=
                { gate := start,
                  hgate := hstart } }.aig.decls[{ aig := aig, ref := { gate := start, hgate := hstart } }.ref.gate] with
    | Decl.const b => b
    | Decl.atom v => assign v
    | Decl.gate lhs rhs linv rinv =>
      let_fun this := ⋯;
      let lval := denote.go lhs { aig := aig, ref := { gate := start, hgate := hstart } }.aig.decls assign ⋯ ⋯;
      let rval := denote.go rhs { aig := aig, ref := { gate := start, hgate := hstart } }.aig.decls assign ⋯ ⋯;
      (lval ^^ linv) && (rval ^^ rinv)) =
    ((denote.go { aig := aig, ref := { gate := lhs, hgate := ⋯ } }.ref.gate
          { aig := aig, ref := { gate := lhs, hgate := ⋯ } }.aig.decls assign ⋯ ⋯ ^^
        linv) &&
      (denote.go { aig := aig, ref := { gate := rhs, hgate := ⋯ } }.ref.gate
          { aig := aig, ref := { gate := rhs, hgate := ⋯ } }.aig.decls assign ⋯ ⋯ ^^
        rinv))
-- Mathlib/Data/Set/NAry.lean
theorem image2_distrib_subset_right {f : δ → γ → ε} {g : α → β → δ} {f₁ : α → γ → α'}
    {f₂ : β → γ → β'} {g' : α' → β' → ε} (h_distrib : ∀ a b c, f (g a b) c = g' (f₁ a c) (f₂ b c)) :
    image2 f (image2 g s t) u ⊆ image2 g' (image2 f₁ s u) (image2 f₂ t u)

Proof state:
case intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
α' : Type u_2
β : Type u_3
β' : Type u_4
γ : Type u_5
δ : Type u_7
ε : Type u_9
s : Set α
t : Set β
u : Set γ
f : δ → γ → ε
g : α → β → δ
f₁ : α → γ → α'
f₂ : β → γ → β'
g' : α' → β' → ε
h_distrib : ∀ (a : α) (b : β) (c : γ), f (g a b) c = g' (f₁ a c) (f₂ b c)
a : α
ha : a ∈ s
b : β
hb : b ∈ t
c : γ
hc : c ∈ u
⊢ g' (f₁ a c) (f₂ b c) ∈ image2 g' (image2 f₁ s u) (image2 f₂ t u)

Tactic:
exact mem_image2_of_mem (mem_image2_of_mem ha hc) (mem_image2_of_mem hb hc)

Result:
no goals

Proof state:
case intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
α' : Type u_2
β : Type u_3
β' : Type u_4
γ : Type u_5
δ : Type u_7
ε : Type u_9
s : Set α
t : Set β
u : Set γ
f : δ → γ → ε
g : α → β → δ
f₁ : α → γ → α'
f₂ : β → γ → β'
g' : α' → β' → ε
h_distrib : ∀ (a : α) (b : β) (c : γ), f (g a b) c = g' (f₁ a c) (f₂ b c)
a : α
ha : a ∈ s
b : β
hb : b ∈ t
c : γ
hc : c ∈ u
⊢ f (g a b) c ∈ image2 g' (image2 f₁ s u) (image2 f₂ t u)

Tactic:
rw [h_distrib]

Result:
case intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
α' : Type u_2
β : Type u_3
β' : Type u_4
γ : Type u_5
δ : Type u_7
ε : Type u_9
s : Set α
t : Set β
u : Set γ
f : δ → γ → ε
g : α → β → δ
f₁ : α → γ → α'
f₂ : β → γ → β'
g' : α' → β' → ε
h_distrib : ∀ (a : α) (b : β) (c : γ), f (g a b) c = g' (f₁ a c) (f₂ b c)
a : α
ha : a ∈ s
b : β
hb : b ∈ t
c : γ
hc : c ∈ u
⊢ g' (f₁ a c) (f₂ b c) ∈ image2 g' (image2 f₁ s u) (image2 f₂ t u)

Proof state:
α : Type u_1
α' : Type u_2
β : Type u_3
β' : Type u_4
γ : Type u_5
δ : Type u_7
ε : Type u_9
s : Set α
t : Set β
u : Set γ
f : δ → γ → ε
g : α → β → δ
f₁ : α → γ → α'
f₂ : β → γ → β'
g' : α' → β' → ε
h_distrib : ∀ (a : α) (b : β) (c : γ), f (g a b) c = g' (f₁ a c) (f₂ b c)
⊢ image2 f (image2 g s t) u ⊆ image2 g' (image2 f₁ s u) (image2 f₂ t u)

Tactic:
rintro _ ⟨_, ⟨a, ha, b, hb, rfl⟩, c, hc, rfl⟩

Result:
case intro.intro.intro.intro.intro.intro.intro.intro
α : Type u_1
α' : Type u_2
β : Type u_3
β' : Type u_4
γ : Type u_5
δ : Type u_7
ε : Type u_9
s : Set α
t : Set β
u : Set γ
f : δ → γ → ε
g : α → β → δ
f₁ : α → γ → α'
f₂ : β → γ → β'
g' : α' → β' → ε
h_distrib : ∀ (a : α) (b : β) (c : γ), f (g a b) c = g' (f₁ a c) (f₂ b c)
a : α
ha : a ∈ s
b : β
hb : b ∈ t
c : γ
hc : c ∈ u
⊢ f (g a b) c ∈ image2 g' (image2 f₁ s u) (image2 f₂ t u)
-- Mathlib/Computability/Tape.lean
theorem Tape.write_mk' {Γ} [Inhabited Γ] (a b : Γ) (L R : ListBlank Γ) :
    (Tape.mk' L (R.cons a)).write b = Tape.mk' L (R.cons b)

Proof state:
Γ : Type u_1
inst✝ : Inhabited Γ
a b : Γ
L R : ListBlank Γ
⊢ write b (mk' L (ListBlank.cons a R)) = mk' L (ListBlank.cons b R)

Tactic:
simp only [Tape.write, Tape.mk', ListBlank.head_cons, ListBlank.tail_cons, eq_self_iff_true,
  and_self_iff]

Result:
no goals
-- Mathlib/Analysis/Convex/Basic.lean
lemma stdSimplex_fin_two :
    stdSimplex 𝕜 (Fin 2) = ([Pi.single 0 1 -[𝕜] Pi.single 1 1] : Set (Fin 2 → 𝕜))

Proof state:
𝕜 : Type u_1
inst✝ : OrderedSemiring 𝕜
⊢ stdSimplex 𝕜 (Fin 2) = [Pi.single 0 1-[𝕜]Pi.single 1 1]

Tactic:
refine Subset.antisymm ?_ (segment_single_subset_stdSimplex 𝕜 (0 : Fin 2) 1)

Result:
𝕜 : Type u_1
inst✝ : OrderedSemiring 𝕜
⊢ stdSimplex 𝕜 (Fin 2) ⊆ [Pi.single 0 1-[𝕜]Pi.single 1 1]

Proof state:
𝕜 : Type u_1
inst✝ : OrderedSemiring 𝕜
⊢ stdSimplex 𝕜 (Fin 2) ⊆ [Pi.single 0 1-[𝕜]Pi.single 1 1]

Tactic:
rintro f ⟨hf₀, hf₁⟩

Result:
case intro
𝕜 : Type u_1
inst✝ : OrderedSemiring 𝕜
f : Fin 2 → 𝕜
hf₀ : ∀ (x : Fin 2), 0 ≤ f x
hf₁ : ∑ x : Fin 2, f x = 1
⊢ f ∈ [Pi.single 0 1-[𝕜]Pi.single 1 1]

Proof state:
case intro
𝕜 : Type u_1
inst✝ : OrderedSemiring 𝕜
f : Fin 2 → 𝕜
hf₀ : ∀ (x : Fin 2), 0 ≤ f x
hf₁ : f 0 + f 1 = 1
⊢ f ∈ [Pi.single 0 1-[𝕜]Pi.single 1 1]

Tactic:
refine ⟨f 0, f 1, hf₀ 0, hf₀ 1, hf₁, funext <| Fin.forall_fin_two.2 ?_⟩

Result:
case intro
𝕜 : Type u_1
inst✝ : OrderedSemiring 𝕜
f : Fin 2 → 𝕜
hf₀ : ∀ (x : Fin 2), 0 ≤ f x
hf₁ : f 0 + f 1 = 1
⊢ (f 0 • Pi.single 0 1 + f 1 • Pi.single 1 1) 0 = f 0 ∧ (f 0 • Pi.single 0 1 + f 1 • Pi.single 1 1) 1 = f 1

Proof state:
case intro
𝕜 : Type u_1
inst✝ : OrderedSemiring 𝕜
f : Fin 2 → 𝕜
hf₀ : ∀ (x : Fin 2), 0 ≤ f x
hf₁ : f 0 + f 1 = 1
⊢ (f 0 • Pi.single 0 1 + f 1 • Pi.single 1 1) 0 = f 0 ∧ (f 0 • Pi.single 0 1 + f 1 • Pi.single 1 1) 1 = f 1

Tactic:
simp

Result:
no goals

Proof state:
case intro
𝕜 : Type u_1
inst✝ : OrderedSemiring 𝕜
f : Fin 2 → 𝕜
hf₀ : ∀ (x : Fin 2), 0 ≤ f x
hf₁ : ∑ x : Fin 2, f x = 1
⊢ f ∈ [Pi.single 0 1-[𝕜]Pi.single 1 1]

Tactic:
rw [Fin.sum_univ_two] at hf₁

Result:
case intro
𝕜 : Type u_1
inst✝ : OrderedSemiring 𝕜
f : Fin 2 → 𝕜
hf₀ : ∀ (x : Fin 2), 0 ≤ f x
hf₁ : f 0 + f 1 = 1
⊢ f ∈ [Pi.single 0 1-[𝕜]Pi.single 1 1]
-- Mathlib/Topology/Constructions.lean
theorem Filter.Tendsto.prod_mk_nhds {γ} {x : X} {y : Y} {f : Filter γ} {mx : γ → X} {my : γ → Y}
    (hx : Tendsto mx f (𝓝 x)) (hy : Tendsto my f (𝓝 y)) :
    Tendsto (fun c => (mx c, my c)) f (𝓝 (x, y))

Proof state:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
γ : Type u_5
x : X
y : Y
f : Filter γ
mx : γ → X
my : γ → Y
hx : Tendsto mx f (𝓝 x)
hy : Tendsto my f (𝓝 y)
⊢ Tendsto (fun c => (mx c, my c)) f (𝓝 (x, y))

Tactic:
rw [nhds_prod_eq]

Result:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
γ : Type u_5
x : X
y : Y
f : Filter γ
mx : γ → X
my : γ → Y
hx : Tendsto mx f (𝓝 x)
hy : Tendsto my f (𝓝 y)
⊢ Tendsto (fun c => (mx c, my c)) f (𝓝 x ×ˢ 𝓝 y)

Proof state:
X : Type u
Y : Type v
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
γ : Type u_5
x : X
y : Y
f : Filter γ
mx : γ → X
my : γ → Y
hx : Tendsto mx f (𝓝 x)
hy : Tendsto my f (𝓝 y)
⊢ Tendsto (fun c => (mx c, my c)) f (𝓝 x ×ˢ 𝓝 y)

Tactic:
exact Filter.Tendsto.prod_mk hx hy

Result:
no goals
-- Mathlib/CategoryTheory/Sites/Coherent/SheafComparison.lean
lemma isSheaf_coherent_of_projective_comp [Preregular C] [FinitaryExtensive C]
    [∀ (X : C), Projective X] [PreservesFiniteProducts s]
    (hF : IsSheaf (coherentTopology C) F) : IsSheaf (coherentTopology C) (F ⋙ s)

Proof state:
C : Type u_1
inst✝⁶ : Category.{u_3, u_1} C
A : Type u₃
inst✝⁵ : Category.{v₃, u₃} A
F : Cᵒᵖ ⥤ A
B : Type u₄
inst✝⁴ : Category.{v₄, u₄} B
s : A ⥤ B
inst✝³ : Preregular C
inst✝² : FinitaryExtensive C
inst✝¹ : ∀ (X : C), Projective X
inst✝ : PreservesFiniteProducts s
hF : IsSheaf (coherentTopology C) F
⊢ IsSheaf (coherentTopology C) (F ⋙ s)

Tactic:
rw [isSheaf_iff_preservesFiniteProducts_of_projective] at hF ⊢

Result:
C : Type u_1
inst✝⁶ : Category.{u_3, u_1} C
A : Type u₃
inst✝⁵ : Category.{v₃, u₃} A
F : Cᵒᵖ ⥤ A
B : Type u₄
inst✝⁴ : Category.{v₄, u₄} B
s : A ⥤ B
inst✝³ : Preregular C
inst✝² : FinitaryExtensive C
inst✝¹ : ∀ (X : C), Projective X
inst✝ : PreservesFiniteProducts s
hF : PreservesFiniteProducts F
⊢ PreservesFiniteProducts (F ⋙ s)

Proof state:
C : Type u_1
inst✝⁶ : Category.{u_3, u_1} C
A : Type u₃
inst✝⁵ : Category.{v₃, u₃} A
F : Cᵒᵖ ⥤ A
B : Type u₄
inst✝⁴ : Category.{v₄, u₄} B
s : A ⥤ B
inst✝³ : Preregular C
inst✝² : FinitaryExtensive C
inst✝¹ : ∀ (X : C), Projective X
inst✝ : PreservesFiniteProducts s
hF : PreservesFiniteProducts F
⊢ PreservesFiniteProducts (F ⋙ s)

Tactic:
infer_instance

Result:
no goals