harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Probability/Kernel/Composition/CompMap.lean
lemma comp_map (κ : Kernel α β) (η : Kernel γ δ) {f : β → γ} (hf : Measurable f) :
    η ∘ₖ (κ.map f) = (η.comap f hf) ∘ₖ κ

Proof state:
case h.h
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel α β
η : Kernel γ δ
f : β → γ
hf : Measurable f
x : α
s : Set δ
ms : MeasurableSet s
⊢ ∫⁻ (a : β), (η (f a)) s ∂κ x = ∫⁻ (b : β), ((η.comap f hf) b) s ∂κ x

Tactic:
simp_rw [comap_apply']

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel α β
η : Kernel γ δ
f : β → γ
hf : Measurable f
⊢ η ∘ₖ κ.map f = η.comap f hf ∘ₖ κ

Tactic:
ext x s ms

Result:
case h.h
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel α β
η : Kernel γ δ
f : β → γ
hf : Measurable f
x : α
s : Set δ
ms : MeasurableSet s
⊢ ((η ∘ₖ κ.map f) x) s = ((η.comap f hf ∘ₖ κ) x) s

Proof state:
case h.h
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel α β
η : Kernel γ δ
f : β → γ
hf : Measurable f
x : α
s : Set δ
ms : MeasurableSet s
⊢ ((η ∘ₖ κ.map f) x) s = ((η.comap f hf ∘ₖ κ) x) s

Tactic:
rw [comp_apply' _ _ _ ms, lintegral_map _ hf _ (η.measurable_coe ms), comp_apply' _ _ _ ms]

Result:
case h.h
α : Type u_1
β : Type u_2
mα : MeasurableSpace α
mβ : MeasurableSpace β
γ : Type u_4
δ : Type u_5
mγ : MeasurableSpace γ
mδ : MeasurableSpace δ
κ : Kernel α β
η : Kernel γ δ
f : β → γ
hf : Measurable f
x : α
s : Set δ
ms : MeasurableSet s
⊢ ∫⁻ (a : β), (η (f a)) s ∂κ x = ∫⁻ (b : β), ((η.comap f hf) b) s ∂κ x
-- Mathlib/LinearAlgebra/AffineSpace/Combination.lean
theorem affineCombination_sdiff_sub [DecidableEq ι] {s₂ : Finset ι} (h : s₂ ⊆ s) (w : ι → k)
    (p : ι → P) :
    (s \ s₂).affineCombination k p w -ᵥ s₂.affineCombination k p (-w) = s.weightedVSub p w

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
inst✝ : DecidableEq ι
s₂ : Finset ι
h : s₂ ⊆ s
w : ι → k
p : ι → P
⊢ (affineCombination k (s \ s₂) p) w -ᵥ (affineCombination k s₂ p) (-w) = (s.weightedVSub p) w

Tactic:
simp_rw [affineCombination_apply, vadd_vsub_vadd_cancel_right]

Result:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
inst✝ : DecidableEq ι
s₂ : Finset ι
h : s₂ ⊆ s
w : ι → k
p : ι → P
⊢ ((s \ s₂).weightedVSubOfPoint p (Classical.choice ⋯)) w - (s₂.weightedVSubOfPoint p (Classical.choice ⋯)) (-w) =
    (s.weightedVSub p) w

Proof state:
k : Type u_1
V : Type u_2
P : Type u_3
inst✝³ : Ring k
inst✝² : AddCommGroup V
inst✝¹ : Module k V
S : AffineSpace V P
ι : Type u_4
s : Finset ι
inst✝ : DecidableEq ι
s₂ : Finset ι
h : s₂ ⊆ s
w : ι → k
p : ι → P
⊢ ((s \ s₂).weightedVSubOfPoint p (Classical.choice ⋯)) w - (s₂.weightedVSubOfPoint p (Classical.choice ⋯)) (-w) =
    (s.weightedVSub p) w

Tactic:
exact s.weightedVSub_sdiff_sub h _ _

Result:
no goals
-- Mathlib/Data/Int/ModEq.lean
theorem modEq_iff_dvd : a ≡ b [ZMOD n] ↔ n ∣ b - a

Proof state:
n a b : ℤ
⊢ a ≡ b [ZMOD n] ↔ n ∣ b - a

Tactic:
rw [ModEq, eq_comm]

Result:
n a b : ℤ
⊢ b % n = a % n ↔ n ∣ b - a

Proof state:
n a b : ℤ
⊢ b % n = a % n ↔ n ∣ b - a

Tactic:
simp [emod_eq_emod_iff_emod_sub_eq_zero, dvd_iff_emod_eq_zero]

Result:
no goals
-- Mathlib/Geometry/Euclidean/Sphere/Basic.lean
protected lemma IsDiameter.wbtw (h : s.IsDiameter p₁ p₂) : Wbtw ℝ p₁ s.center p₂

Proof state:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Sphere P
p₁ p₂ : P
h : s.IsDiameter p₁ p₂
⊢ Wbtw ℝ p₁ s.center p₂

Tactic:
rw [← h.midpoint_eq_center]

Result:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Sphere P
p₁ p₂ : P
h : s.IsDiameter p₁ p₂
⊢ Wbtw ℝ p₁ (midpoint ℝ p₁ p₂) p₂

Proof state:
V : Type u_1
P : Type u_2
inst✝³ : NormedAddCommGroup V
inst✝² : NormedSpace ℝ V
inst✝¹ : MetricSpace P
inst✝ : NormedAddTorsor V P
s : Sphere P
p₁ p₂ : P
h : s.IsDiameter p₁ p₂
⊢ Wbtw ℝ p₁ (midpoint ℝ p₁ p₂) p₂

Tactic:
exact wbtw_midpoint _ _ _

Result:
no goals
-- Mathlib/RingTheory/UniqueFactorizationDomain/NormalizedFactors.lean
theorem normalizedFactors_of_irreducible_pow {p : α} (hp : Irreducible p) (k : ℕ) :
    normalizedFactors (p ^ k) = Multiset.replicate k (normalize p)

Proof state:
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
p : α
hp : Irreducible p
k : ℕ
⊢ normalizedFactors (p ^ k) = Multiset.replicate k (normalize p)

Tactic:
rw [normalizedFactors_pow, normalizedFactors_irreducible hp, Multiset.nsmul_singleton]

Result:
no goals
-- Mathlib/Analysis/NormedSpace/OperatorNorm/Basic.lean
theorem isLeast_opNorm [RingHomIsometric σ₁₂] (f : E →SL[σ₁₂] F) :
    IsLeast {c | 0 ≤ c ∧ ∀ x, ‖f x‖ ≤ c * ‖x‖} ‖f‖

Proof state:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst✝⁶ : SeminormedAddCommGroup E
inst✝⁵ : SeminormedAddCommGroup F
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NontriviallyNormedField 𝕜₂
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝ : RingHomIsometric σ₁₂
f : E →SL[σ₁₂] F
⊢ IsClosed ({a | 0 ≤ a} ∩ ⋂ i, {x | ‖f i‖ ≤ x * ‖i‖})

Tactic:
refine isClosed_Ici.inter <| isClosed_iInter fun _ ↦ isClosed_le ?_ ?_ <;> continuity

Result:
no goals

Proof state:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst✝⁶ : SeminormedAddCommGroup E
inst✝⁵ : SeminormedAddCommGroup F
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NontriviallyNormedField 𝕜₂
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝ : RingHomIsometric σ₁₂
f : E →SL[σ₁₂] F
⊢ IsLeast {c | 0 ≤ c ∧ ∀ (x : E), ‖f x‖ ≤ c * ‖x‖} ‖f‖

Tactic:
refine IsClosed.isLeast_csInf ?_ bounds_nonempty bounds_bddBelow

Result:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst✝⁶ : SeminormedAddCommGroup E
inst✝⁵ : SeminormedAddCommGroup F
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NontriviallyNormedField 𝕜₂
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝ : RingHomIsometric σ₁₂
f : E →SL[σ₁₂] F
⊢ IsClosed {c | 0 ≤ c ∧ ∀ (x : E), ‖f x‖ ≤ c * ‖x‖}

Proof state:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst✝⁶ : SeminormedAddCommGroup E
inst✝⁵ : SeminormedAddCommGroup F
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NontriviallyNormedField 𝕜₂
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝ : RingHomIsometric σ₁₂
f : E →SL[σ₁₂] F
⊢ IsClosed {c | 0 ≤ c ∧ ∀ (x : E), ‖f x‖ ≤ c * ‖x‖}

Tactic:
simp only [setOf_and, setOf_forall]

Result:
𝕜 : Type u_1
𝕜₂ : Type u_2
E : Type u_4
F : Type u_5
inst✝⁶ : SeminormedAddCommGroup E
inst✝⁵ : SeminormedAddCommGroup F
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NontriviallyNormedField 𝕜₂
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedSpace 𝕜₂ F
σ₁₂ : 𝕜 →+* 𝕜₂
inst✝ : RingHomIsometric σ₁₂
f : E →SL[σ₁₂] F
⊢ IsClosed ({a | 0 ≤ a} ∩ ⋂ i, {x | ‖f i‖ ≤ x * ‖i‖})
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem getElem?_reverse {l : List α} {i} (h : i < length l) :
    l.reverse[i]? = l[l.length - 1 - i]? :=
  getElem?_reverse' _ _ <| by
    rw [Nat.add_sub_of_le (Nat.le_sub_one_of_lt h),
      Nat.sub_add_cancel (Nat.lt_of_le_of_lt (Nat.zero_le _) h)]

Proof state:
α : Type u_1
l : List α
i : Nat
h : i < l.length
⊢ i + (l.length - 1 - i) + 1 = l.length

Tactic:
rw [Nat.add_sub_of_le (Nat.le_sub_one_of_lt h),
  Nat.sub_add_cancel (Nat.lt_of_le_of_lt (Nat.zero_le _) h)]

Result:
no goals
-- Mathlib/Algebra/Polynomial/Monic.lean
theorem Monic.sub_of_left {p q : R[X]} (hp : Monic p) (hpq : degree q < degree p) :
    Monic (p - q)

Proof state:
R : Type u
inst✝ : Ring R
p q : R[X]
hp : p.Monic
hpq : q.degree < p.degree
⊢ (-q).degree < p.degree

Tactic:
rwa [degree_neg]

Result:
no goals

Proof state:
R : Type u
inst✝ : Ring R
p q : R[X]
hp : p.Monic
hpq : q.degree < p.degree
⊢ (p - q).Monic

Tactic:
rw [sub_eq_add_neg]

Result:
R : Type u
inst✝ : Ring R
p q : R[X]
hp : p.Monic
hpq : q.degree < p.degree
⊢ (p + -q).Monic

Proof state:
R : Type u
inst✝ : Ring R
p q : R[X]
hp : p.Monic
hpq : q.degree < p.degree
⊢ (p + -q).Monic

Tactic:
apply hp.add_of_left

Result:
R : Type u
inst✝ : Ring R
p q : R[X]
hp : p.Monic
hpq : q.degree < p.degree
⊢ (-q).degree < p.degree
-- Mathlib/Algebra/Group/AddChar.lean
@[simp]
lemma mulShift_one (ψ : AddChar R M) : mulShift ψ 1 = ψ

Proof state:
R : Type u_1
M : Type u_2
inst✝¹ : Ring R
inst✝ : CommMonoid M
ψ : AddChar R M
⊢ ψ.mulShift 1 = ψ

Tactic:
ext

Result:
case h
R : Type u_1
M : Type u_2
inst✝¹ : Ring R
inst✝ : CommMonoid M
ψ : AddChar R M
x✝ : R
⊢ (ψ.mulShift 1) x✝ = ψ x✝

Proof state:
case h
R : Type u_1
M : Type u_2
inst✝¹ : Ring R
inst✝ : CommMonoid M
ψ : AddChar R M
x✝ : R
⊢ (ψ.mulShift 1) x✝ = ψ x✝

Tactic:
rw [mulShift_apply, one_mul]

Result:
no goals
-- Mathlib/Combinatorics/Quiver/Covering.lean
theorem Prefunctor.IsCovering.map_injective (hφ : φ.IsCovering) {u v : U} :
    Injective fun f : u ⟶ v => φ.map f

Proof state:
U : Type u_1
inst✝¹ : Quiver U
V : Type u_2
inst✝ : Quiver V
φ : U ⥤q V
hφ : φ.IsCovering
u v : U
f g : u ⟶ v
he : (fun f => φ.map f) f = (fun f => φ.map f) g
this : φ.star u (Star.mk f) = φ.star u (Star.mk g)
⊢ f = g

Tactic:
simpa using (hφ.star_bijective u).left this

Result:
no goals

Proof state:
U : Type u_1
inst✝¹ : Quiver U
V : Type u_2
inst✝ : Quiver V
φ : U ⥤q V
hφ : φ.IsCovering
u v : U
f g : u ⟶ v
he : (fun f => φ.map f) f = (fun f => φ.map f) g
⊢ φ.star u (Star.mk f) = φ.star u (Star.mk g)

Tactic:
simpa using he

Result:
no goals

Proof state:
U : Type u_1
inst✝¹ : Quiver U
V : Type u_2
inst✝ : Quiver V
φ : U ⥤q V
hφ : φ.IsCovering
u v : U
⊢ Injective fun f => φ.map f

Tactic:
rintro f g he

Result:
U : Type u_1
inst✝¹ : Quiver U
V : Type u_2
inst✝ : Quiver V
φ : U ⥤q V
hφ : φ.IsCovering
u v : U
f g : u ⟶ v
he : (fun f => φ.map f) f = (fun f => φ.map f) g
⊢ f = g

Proof state:
U : Type u_1
inst✝¹ : Quiver U
V : Type u_2
inst✝ : Quiver V
φ : U ⥤q V
hφ : φ.IsCovering
u v : U
f g : u ⟶ v
he : (fun f => φ.map f) f = (fun f => φ.map f) g
⊢ f = g

Tactic:
have : φ.star u (Quiver.Star.mk f) = φ.star u (Quiver.Star.mk g) := by simpa using he

Result:
U : Type u_1
inst✝¹ : Quiver U
V : Type u_2
inst✝ : Quiver V
φ : U ⥤q V
hφ : φ.IsCovering
u v : U
f g : u ⟶ v
he : (fun f => φ.map f) f = (fun f => φ.map f) g
this : φ.star u (Star.mk f) = φ.star u (Star.mk g)
⊢ f = g
-- Mathlib/Algebra/Polynomial/FieldDivision.lean
theorem prime_of_degree_eq_one (hp1 : degree p = 1) : Prime p

Proof state:
R : Type u
inst✝ : Field R
p : R[X]
hp1 : p.degree = 1
this : Prime (normalize p)
⊢ Prime p

Tactic:
exact (normalize_associated _).prime this

Result:
no goals

Proof state:
R : Type u
inst✝ : Field R
p : R[X]
hp1 : p.degree = 1
⊢ Prime p

Tactic:
have : Prime (normalize p) :=
  Monic.prime_of_degree_eq_one (hp1 ▸ degree_normalize)
    (monic_normalize fun hp0 => absurd hp1 (hp0.symm ▸ by simp [degree_zero]))

Result:
R : Type u
inst✝ : Field R
p : R[X]
hp1 : p.degree = 1
this : Prime (normalize p)
⊢ Prime p

Proof state:
R : Type u
inst✝ : Field R
p : R[X]
hp1 : p.degree = 1
hp0 : p = 0
⊢ ¬degree 0 = 1

Tactic:
simp [degree_zero]

Result:
no goals

Proof state:
R : Type u
inst✝ : Field R
p : R[X]
hp1 : p.degree = 1
⊢ Prime p

Tactic:
classical
have : Prime (normalize p) :=
  Monic.prime_of_degree_eq_one (hp1 ▸ degree_normalize)
    (monic_normalize fun hp0 => absurd hp1 (hp0.symm ▸ by simp [degree_zero]))
exact (normalize_associated _).prime this

Result:
no goals
-- Mathlib/MeasureTheory/Function/Jacobian.lean
lemma _root_.MeasurableEquiv.withDensity_ofReal_map_symm_apply_eq_integral_abs_deriv_mul'
    (f : ℝ ≃ᵐ ℝ) {s : Set ℝ} (hs : MeasurableSet s)
    {f' : ℝ → ℝ} (hf' : ∀ x, HasDerivAt f (f' x) x)
    {g : ℝ → ℝ} (hg : 0 ≤ᵐ[volume] g) (hg_int : Integrable g) :
    (volume.withDensity (fun x ↦ ENNReal.ofReal (g x))).map f.symm s
      = ENNReal.ofReal (∫ x in s, |f' x| * g (f x))

Proof state:
f : ℝ ≃ᵐ ℝ
s : Set ℝ
hs : MeasurableSet s
f' : ℝ → ℝ
hf' : ∀ (x : ℝ), HasDerivAt (⇑f) (f' x) x
g : ℝ → ℝ
hg : 0 ≤ᶠ[ae volume] g
hg_int : Integrable g volume
⊢ (Measure.map (⇑f.symm) (volume.withDensity fun x => ENNReal.ofReal (g x))) s =
    ENNReal.ofReal (∫ (x : ℝ) in s, |f' x| * g (f x))

Tactic:
rw [MeasurableEquiv.withDensity_ofReal_map_symm_apply_eq_integral_abs_det_fderiv_mul volume hs
    f (by filter_upwards [hg] with x hx using fun _ ↦ hx) hg_int.integrableOn
    (fun x _ => (hf' x).hasDerivWithinAt)]

Result:
f : ℝ ≃ᵐ ℝ
s : Set ℝ
hs : MeasurableSet s
f' : ℝ → ℝ
hf' : ∀ (x : ℝ), HasDerivAt (⇑f) (f' x) x
g : ℝ → ℝ
hg : 0 ≤ᶠ[ae volume] g
hg_int : Integrable g volume
⊢ ENNReal.ofReal (∫ (x : ℝ) in s, |(ContinuousLinearMap.smulRight 1 (f' x)).det| * g (f x)) =
    ENNReal.ofReal (∫ (x : ℝ) in s, |f' x| * g (f x))

Proof state:
f : ℝ ≃ᵐ ℝ
s : Set ℝ
hs : MeasurableSet s
f' : ℝ → ℝ
hf' : ∀ (x : ℝ), HasDerivAt (⇑f) (f' x) x
g : ℝ → ℝ
hg : 0 ≤ᶠ[ae volume] g
hg_int : Integrable g volume
⊢ ∀ᵐ (x : ℝ), x ∈ ⇑f '' s → 0 ≤ g x

Tactic:
filter_upwards [hg] with x hx using fun _ ↦ hx

Result:
no goals

Proof state:
f : ℝ ≃ᵐ ℝ
s : Set ℝ
hs : MeasurableSet s
f' : ℝ → ℝ
hf' : ∀ (x : ℝ), HasDerivAt (⇑f) (f' x) x
g : ℝ → ℝ
hg : 0 ≤ᶠ[ae volume] g
hg_int : Integrable g volume
⊢ ENNReal.ofReal (∫ (x : ℝ) in s, |(ContinuousLinearMap.smulRight 1 (f' x)).det| * g (f x)) =
    ENNReal.ofReal (∫ (x : ℝ) in s, |f' x| * g (f x))

Tactic:
simp only [det_one_smulRight]

Result:
no goals
-- Mathlib/Data/Fin/Basic.lean
@[simp] lemma predAbove_zero_of_ne_zero [NeZero n] {i : Fin (n + 1)} (hi : i ≠ 0) :
    predAbove 0 i = i.pred hi

Proof state:
case intro
n : ℕ
inst✝ : NeZero n
y : Fin n
hi : y.succ ≠ 0
⊢ predAbove 0 y.succ = y.succ.pred hi

Tactic:
exact predAbove_zero_succ

Result:
no goals

Proof state:
n : ℕ
inst✝ : NeZero n
i : Fin (n + 1)
hi : i ≠ 0
⊢ predAbove 0 i = i.pred hi

Tactic:
obtain ⟨y, rfl⟩ := exists_succ_eq.2 hi

Result:
case intro
n : ℕ
inst✝ : NeZero n
y : Fin n
hi : y.succ ≠ 0
⊢ predAbove 0 y.succ = y.succ.pred hi
-- Mathlib/Topology/Maps/Basic.lean
lemma closure_eq_preimage_closure_image (hf : IsInducing f) (s : Set X) :
    closure s = f ⁻¹' closure (f '' s)

Proof state:
X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace X
hf : IsInducing f
s : Set X
⊢ closure s = f ⁻¹' closure (f '' s)

Tactic:
ext x

Result:
case h
X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace X
hf : IsInducing f
s : Set X
x : X
⊢ x ∈ closure s ↔ x ∈ f ⁻¹' closure (f '' s)

Proof state:
case h
X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace Y
inst✝ : TopologicalSpace X
hf : IsInducing f
s : Set X
x : X
⊢ x ∈ closure s ↔ x ∈ f ⁻¹' closure (f '' s)

Tactic:
rw [Set.mem_preimage, ← closure_induced, hf.eq_induced]

Result:
no goals
-- Mathlib/GroupTheory/Perm/Cycle/Concrete.lean
theorem two_le_length_toList_iff_mem_support {p : Perm α} {x : α} :
    2 ≤ length (toList p x) ↔ x ∈ p.support

Proof state:
α : Type u_1
inst✝¹ : Fintype α
inst✝ : DecidableEq α
p : Perm α
x : α
⊢ 2 ≤ (p.toList x).length ↔ x ∈ p.support

Tactic:
simp

Result:
no goals
-- Mathlib/CategoryTheory/Limits/Shapes/Pullback/CommSq.lean
/-- The following diagram is a pullback
```
X --id--> X
|         |
f         f
v         v
Z --id--> Z
```
-/
lemma id_horiz (f : X ⟶ Z) : IsPullback (𝟙 X) f f (𝟙 Z) :=
  of_horiz_isIso ⟨by simp only [Category.id_comp, Category.comp_id]⟩

Proof state:
C : Type u₁
inst✝ : Category.{v₁, u₁} C
X Z : C
f : X ⟶ Z
⊢ 𝟙 X ≫ f = f ≫ 𝟙 Z

Tactic:
simp only [Category.id_comp, Category.comp_id]

Result:
no goals
-- Mathlib/Order/SuccPred/CompleteLinearOrder.lean
lemma csInf_mem_of_not_isPredPrelimit
    (hne : s.Nonempty) (hbdd : BddBelow s) (hlim : ¬ IsPredPrelimit (sInf s)) : sInf s ∈ s

Proof state:
case intro
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
s : Set α
hne : s.Nonempty
hbdd : BddBelow s
hlim : ¬IsPredPrelimit (sInf s)
y : α
hy : sInf s ⋖ y
⊢ sInf s ∈ s

Tactic:
obtain ⟨i, his, hi⟩ := exists_lt_of_csInf_lt hne hy.lt

Result:
case intro.intro.intro
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
s : Set α
hne : s.Nonempty
hbdd : BddBelow s
hlim : ¬IsPredPrelimit (sInf s)
y : α
hy : sInf s ⋖ y
i : α
his : i ∈ s
hi : i < y
⊢ sInf s ∈ s

Proof state:
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
s : Set α
hne : s.Nonempty
hbdd : BddBelow s
hlim : ¬IsPredPrelimit (sInf s)
⊢ sInf s ∈ s

Tactic:
obtain ⟨y, hy⟩ := not_forall_not.mp hlim

Result:
case intro
α : Type u_2
inst✝ : ConditionallyCompleteLinearOrder α
s : Set α
hne : s.Nonempty
hbdd : BddBelow s
hlim : ¬IsPredPrelimit (sInf s)
y : α
hy : sInf s ⋖ y
⊢ sInf s ∈ s
-- Mathlib/Data/Matrix/Block.lean
theorem fromBlocks_multiply [Fintype l] [Fintype m] [NonUnitalNonAssocSemiring α] (A : Matrix n l α)
    (B : Matrix n m α) (C : Matrix o l α) (D : Matrix o m α) (A' : Matrix l p α) (B' : Matrix l q α)
    (C' : Matrix m p α) (D' : Matrix m q α) :
    fromBlocks A B C D * fromBlocks A' B' C' D' =
      fromBlocks (A * A' + B * C') (A * B' + B * D') (C * A' + D * C') (C * B' + D * D')

Proof state:
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
q : Type u_6
α : Type u_12
inst✝² : Fintype l
inst✝¹ : Fintype m
inst✝ : NonUnitalNonAssocSemiring α
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
A' : Matrix l p α
B' : Matrix l q α
C' : Matrix m p α
D' : Matrix m q α
⊢ fromBlocks A B C D * fromBlocks A' B' C' D' =
    fromBlocks (A * A' + B * C') (A * B' + B * D') (C * A' + D * C') (C * B' + D * D')

Tactic:
ext i j

Result:
case a
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
q : Type u_6
α : Type u_12
inst✝² : Fintype l
inst✝¹ : Fintype m
inst✝ : NonUnitalNonAssocSemiring α
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
A' : Matrix l p α
B' : Matrix l q α
C' : Matrix m p α
D' : Matrix m q α
i : n ⊕ o
j : p ⊕ q
⊢ (fromBlocks A B C D * fromBlocks A' B' C' D') i j =
    fromBlocks (A * A' + B * C') (A * B' + B * D') (C * A' + D * C') (C * B' + D * D') i j

Proof state:
case a
l : Type u_1
m : Type u_2
n : Type u_3
o : Type u_4
p : Type u_5
q : Type u_6
α : Type u_12
inst✝² : Fintype l
inst✝¹ : Fintype m
inst✝ : NonUnitalNonAssocSemiring α
A : Matrix n l α
B : Matrix n m α
C : Matrix o l α
D : Matrix o m α
A' : Matrix l p α
B' : Matrix l q α
C' : Matrix m p α
D' : Matrix m q α
i : n ⊕ o
j : p ⊕ q
⊢ (fromBlocks A B C D * fromBlocks A' B' C' D') i j =
    fromBlocks (A * A' + B * C') (A * B' + B * D') (C * A' + D * C') (C * B' + D * D') i j

Tactic:
rcases i with ⟨⟩ <;> rcases j with ⟨⟩ <;> simp only [fromBlocks, mul_apply, of_apply,
    Sum.elim_inr, Fintype.sum_sum_type, Sum.elim_inl, add_apply]

Result:
no goals
-- Mathlib/GroupTheory/Submonoid/Centralizer.lean
@[to_additive (attr := simp)]
lemma centralizer_centralizer_centralizer {s : Set M} :
    centralizer s.centralizer.centralizer = centralizer s

Proof state:
M : Type u_1
inst✝ : Monoid M
s : Set M
⊢ centralizer s.centralizer.centralizer = centralizer s

Tactic:
apply SetLike.coe_injective

Result:
case a
M : Type u_1
inst✝ : Monoid M
s : Set M
⊢ ↑(centralizer s.centralizer.centralizer) = ↑(centralizer s)

Proof state:
case a
M : Type u_1
inst✝ : Monoid M
s : Set M
⊢ ↑(centralizer s.centralizer.centralizer) = ↑(centralizer s)

Tactic:
simp only [coe_centralizer, Set.centralizer_centralizer_centralizer]

Result:
no goals
-- Mathlib/GroupTheory/SemidirectProduct.lean
theorem lift_inl (n : N) : lift fn fg h (inl n) = fn n

Proof state:
N : Type u_1
G : Type u_2
H : Type u_3
inst✝² : Group N
inst✝¹ : Group G
inst✝ : Group H
φ : G →* MulAut N
fn : N →* H
fg : G →* H
h : ∀ (g : G), fn.comp (MulEquiv.toMonoidHom (φ g)) = (MulEquiv.toMonoidHom (MulAut.conj (fg g))).comp fn
n : N
⊢ (lift fn fg h) (inl n) = fn n

Tactic:
simp [lift]

Result:
no goals
-- Mathlib/Order/Minimal.lean
theorem map_maximal_mem (f : s ≃o t) (hx : Maximal (· ∈ s) x) :
    Maximal (· ∈ t) (f ⟨x, hx.prop⟩)

Proof state:
α : Type u_1
x : α
inst✝¹ : Preorder α
β : Type u_2
inst✝ : Preorder β
s : Set α
t : Set β
f : ↑s ≃o ↑t
hx : Maximal (fun x => x ∈ s) x
⊢ Maximal (fun x => x ∈ t) ↑(f ⟨x, ⋯⟩)

Tactic:
simpa only [show t = range (Subtype.val ∘ f) by simp, mem_univ, maximal_true_subtype, hx,
  true_imp_iff, image_univ] using OrderEmbedding.maximal_mem_image
  (f.toOrderEmbedding.trans (OrderEmbedding.subtype t)) (s := univ) (x := ⟨x, hx.prop⟩)

Result:
no goals

Proof state:
α : Type u_1
x : α
inst✝¹ : Preorder α
β : Type u_2
inst✝ : Preorder β
s : Set α
t : Set β
f : ↑s ≃o ↑t
hx : Maximal (fun x => x ∈ s) x
⊢ t = range (Subtype.val ∘ ⇑f)

Tactic:
simp

Result:
no goals
-- Mathlib/AlgebraicGeometry/EllipticCurve/Affine.lean
lemma map_negPolynomial :
    (W'.map f).toAffine.negPolynomial = W'.negPolynomial.map (mapRingHom f)

Proof state:
R : Type r
S : Type s
inst✝¹ : CommRing R
inst✝ : CommRing S
W' : Affine R
f : R →+* S
⊢ (map W' f).toAffine.negPolynomial = Polynomial.map (mapRingHom f) W'.negPolynomial

Tactic:
simp only [negPolynomial]

Result:
R : Type r
S : Type s
inst✝¹ : CommRing R
inst✝ : CommRing S
W' : Affine R
f : R →+* S
⊢ -Y - C (C (map W' f).toAffine.a₁ * X + C (map W' f).toAffine.a₃) =
    Polynomial.map (mapRingHom f) (-Y - C (C W'.a₁ * X + C W'.a₃))

Proof state:
R : Type r
S : Type s
inst✝¹ : CommRing R
inst✝ : CommRing S
W' : Affine R
f : R →+* S
⊢ -Y - C (C (map W' f).toAffine.a₁ * X + C (map W' f).toAffine.a₃) =
    Polynomial.map (mapRingHom f) (-Y - C (C W'.a₁ * X + C W'.a₃))

Tactic:
map_simp

Result:
no goals
-- Mathlib/Algebra/Homology/ShortComplex/HomologicalComplex.lean
lemma isIso_homologyι : IsIso (K.homologyι i) :=
  ShortComplex.isIso_homologyι _ (by aesop_cat)

Proof state:
C : Type u_1
inst✝² : Category.{u_3, u_1} C
inst✝¹ : HasZeroMorphisms C
ι : Type u_2
c : ComplexShape ι
K : HomologicalComplex C c
i j : ι
hj : c.next i = j
h : K.d i j = 0
inst✝ : K.HasHomology i
⊢ (K.sc i).g = 0

Tactic:
aesop_cat

Result:
no goals
-- Mathlib/Data/ZMod/Basic.lean
theorem intCast_eq_iff (p : ℕ) (n : ℤ) (z : ZMod p) [NeZero p] :
    ↑n = z ↔ ∃ k, n = z.val + p * k

Proof state:
case mpr
p : ℕ
n : ℤ
z : ZMod p
inst✝ : NeZero p
⊢ (∃ k, n = ↑z.val + ↑p * k) → ↑n = z

Tactic:
rintro ⟨k, rfl⟩

Result:
case mpr.intro
p : ℕ
z : ZMod p
inst✝ : NeZero p
k : ℤ
⊢ ↑(↑z.val + ↑p * k) = z

Proof state:
case mp
p : ℕ
n : ℤ
z : ZMod p
inst✝ : NeZero p
⊢ ↑n = z → ∃ k, n = ↑z.val + ↑p * k

Tactic:
rintro rfl

Result:
case mp
p : ℕ
n : ℤ
inst✝ : NeZero p
⊢ ∃ k, n = ↑(↑n).val + ↑p * k

Proof state:
case mpr.intro
p : ℕ
z : ZMod p
inst✝ : NeZero p
k : ℤ
⊢ ↑(↑z.val + ↑p * k) = z

Tactic:
rw [Int.cast_add, Int.cast_mul, Int.cast_natCast, Int.cast_natCast, natCast_val,
  ZMod.natCast_self, zero_mul, add_zero, cast_id]

Result:
no goals

Proof state:
case mp
p : ℕ
n : ℤ
inst✝ : NeZero p
⊢ ∃ k, n = ↑(↑n).val + ↑p * k

Tactic:
refine ⟨n / p, ?_⟩

Result:
case mp
p : ℕ
n : ℤ
inst✝ : NeZero p
⊢ n = ↑(↑n).val + ↑p * (n / ↑p)

Proof state:
p : ℕ
n : ℤ
z : ZMod p
inst✝ : NeZero p
⊢ ↑n = z ↔ ∃ k, n = ↑z.val + ↑p * k

Tactic:
constructor

Result:
case mp
p : ℕ
n : ℤ
z : ZMod p
inst✝ : NeZero p
⊢ ↑n = z → ∃ k, n = ↑z.val + ↑p * k

case mpr
p : ℕ
n : ℤ
z : ZMod p
inst✝ : NeZero p
⊢ (∃ k, n = ↑z.val + ↑p * k) → ↑n = z

Proof state:
case mp
p : ℕ
n : ℤ
inst✝ : NeZero p
⊢ n = ↑(↑n).val + ↑p * (n / ↑p)

Tactic:
rw [val_intCast, Int.emod_add_ediv]

Result:
no goals