harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Topology/Category/LightProfinite/Extend.lean
theorem functor_initial (hc : IsLimit c) [∀ i, Epi (c.π.app i)] : Initial (functor c)

Proof state:
F : ℕᵒᵖ ⥤ FintypeCat
c : Cone (F ⋙ toLightProfinite)
hc : IsLimit c
inst✝ : ∀ (i : ℕᵒᵖ), Epi (c.π.app i)
⊢ (functor c).Initial

Tactic:
rw [initial_iff_comp_equivalence _ (StructuredArrow.post _ _ lightToProfinite)]

Result:
F : ℕᵒᵖ ⥤ FintypeCat
c : Cone (F ⋙ toLightProfinite)
hc : IsLimit c
inst✝ : ∀ (i : ℕᵒᵖ), Epi (c.π.app i)
⊢ (functor c ⋙ StructuredArrow.post c.pt toLightProfinite lightToProfinite).Initial

Proof state:
F : ℕᵒᵖ ⥤ FintypeCat
c : Cone (F ⋙ toLightProfinite)
hc : IsLimit c
inst✝ : ∀ (i : ℕᵒᵖ), Epi (c.π.app i)
⊢ (functor c ⋙ StructuredArrow.post c.pt toLightProfinite lightToProfinite).Initial

Tactic:
have : ∀ i, Epi ((lightToProfinite.mapCone c).π.app i) :=
  fun i ↦ inferInstanceAs (Epi (lightToProfinite.map (c.π.app i)))

Result:
F : ℕᵒᵖ ⥤ FintypeCat
c : Cone (F ⋙ toLightProfinite)
hc : IsLimit c
inst✝ : ∀ (i : ℕᵒᵖ), Epi (c.π.app i)
this : ∀ (i : ℕᵒᵖ), Epi ((lightToProfinite.mapCone c).π.app i)
⊢ (functor c ⋙ StructuredArrow.post c.pt toLightProfinite lightToProfinite).Initial

Proof state:
F : ℕᵒᵖ ⥤ FintypeCat
c : Cone (F ⋙ toLightProfinite)
hc : IsLimit c
inst✝ : ∀ (i : ℕᵒᵖ), Epi (c.π.app i)
this : ∀ (i : ℕᵒᵖ), Epi ((lightToProfinite.mapCone c).π.app i)
⊢ (functor c ⋙ StructuredArrow.post c.pt toLightProfinite lightToProfinite).Initial

Tactic:
exact Profinite.Extend.functor_initial _ (isLimitOfPreserves lightToProfinite hc)

Result:
no goals
-- Mathlib/RingTheory/UniqueFactorizationDomain/NormalizedFactors.lean
theorem dvd_of_mem_normalizedFactors {a p : α} (H : p ∈ normalizedFactors a) : p ∣ a

Proof state:
case neg
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
a p : α
H : p ∈ normalizedFactors a
hcases : ¬a = 0
⊢ p ∣ a

Tactic:
exact dvd_trans (Multiset.dvd_prod H) (Associated.dvd (prod_normalizedFactors hcases))

Result:
no goals

Proof state:
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
a p : α
H : p ∈ normalizedFactors a
⊢ p ∣ a

Tactic:
by_cases hcases : a = 0

Result:
case pos
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
a p : α
H : p ∈ normalizedFactors a
hcases : a = 0
⊢ p ∣ a

case neg
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
a p : α
H : p ∈ normalizedFactors a
hcases : ¬a = 0
⊢ p ∣ a

Proof state:
case pos
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
a p : α
H : p ∈ normalizedFactors a
hcases : a = 0
⊢ p ∣ a

Tactic:
rw [hcases]

Result:
case pos
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
a p : α
H : p ∈ normalizedFactors a
hcases : a = 0
⊢ p ∣ 0

Proof state:
case pos
α : Type u_1
inst✝² : CancelCommMonoidWithZero α
inst✝¹ : NormalizationMonoid α
inst✝ : UniqueFactorizationMonoid α
a p : α
H : p ∈ normalizedFactors a
hcases : a = 0
⊢ p ∣ 0

Tactic:
exact dvd_zero p

Result:
no goals
-- Mathlib/Algebra/Group/Pointwise/Set/Basic.lean
theorem preimage_mul_right_one' : (· * b⁻¹) ⁻¹' 1 = {b}

Proof state:
α : Type u_2
inst✝ : Group α
b : α
⊢ (fun x => x * b⁻¹) ⁻¹' 1 = {b}

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Ring/Units.lean
theorem divp_sub_divp_same (a b : α) (u : αˣ) : a /ₚ u - b /ₚ u = (a - b) /ₚ u

Proof state:
α : Type u
inst✝ : Ring α
a b : α
u : αˣ
⊢ a /ₚ u - b /ₚ u = (a - b) /ₚ u

Tactic:
rw [sub_eq_add_neg, sub_eq_add_neg, neg_divp, divp_add_divp_same]

Result:
no goals
-- Mathlib/Algebra/Order/Field/Power.lean
theorem zpow_le_max_iff_min_le {x : α} (hx : 1 < x) {a b c : ℤ} :
    x ^ (-c) ≤ max (x ^ (-a)) (x ^ (-b)) ↔ min a b ≤ c

Proof state:
α : Type u_1
inst✝ : LinearOrderedSemifield α
x : α
hx : 1 < x
a b c : ℤ
⊢ x ^ (-c) ≤ x ^ (-a) ⊔ x ^ (-b) ↔ a ⊓ b ≤ c

Tactic:
simp_rw [le_max_iff, min_le_iff, zpow_le_zpow_iff_right₀ hx, neg_le_neg_iff]

Result:
no goals
-- Mathlib/Analysis/Asymptotics/TVS.lean
@[simp]
lemma IsLittleOTVS.bot : f =o[𝕜;⊥] g :=
  fun u hU => ⟨univ, by simp⟩

Proof state:
α : Type u_1
𝕜 : Type u_3
E : Type u_4
F : Type u_5
inst✝⁶ : NontriviallyNormedField 𝕜
inst✝⁵ : AddCommGroup E
inst✝⁴ : TopologicalSpace E
inst✝³ : Module 𝕜 E
inst✝² : AddCommGroup F
inst✝¹ : TopologicalSpace F
inst✝ : Module 𝕜 F
f : α → E
g : α → F
u : Set E
hU : u ∈ 𝓝 0
⊢ univ ∈ 𝓝 0 ∧ ∀ (ε : ℝ≥0), ε ≠ 0 → ∀ᶠ (x : α) in ⊥, egauge 𝕜 u (f x) ≤ ↑ε * egauge 𝕜 univ (g x)

Tactic:
simp

Result:
no goals
-- Mathlib/Geometry/RingedSpace/SheafedSpace.lean
theorem congr_app {X Y : SheafedSpace C} {α β : X ⟶ Y} (h : α = β) (U) :
    α.c.app U = β.c.app U ≫ X.presheaf.map (eqToHom (by subst h; rfl)) :=
  PresheafedSpace.congr_app h U

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X Y : SheafedSpace C
α : X ⟶ Y
U : (Opens ↑↑Y.toPresheafedSpace)ᵒᵖ
⊢ (Opens.map α.base).op.obj U = (Opens.map α.base).op.obj U

Tactic:
rfl

Result:
no goals

Proof state:
C : Type u
inst✝ : Category.{v, u} C
X Y : SheafedSpace C
α β : X ⟶ Y
h : α = β
U : (Opens ↑↑Y.toPresheafedSpace)ᵒᵖ
⊢ (Opens.map β.base).op.obj U = (Opens.map α.base).op.obj U

Tactic:
subst h

Result:
C : Type u
inst✝ : Category.{v, u} C
X Y : SheafedSpace C
α : X ⟶ Y
U : (Opens ↑↑Y.toPresheafedSpace)ᵒᵖ
⊢ (Opens.map α.base).op.obj U = (Opens.map α.base).op.obj U
-- Mathlib/Algebra/Group/Subsemigroup/Basic.lean
theorem iSup_eq_closure {ι : Sort*} (p : ι → Subsemigroup M) :
    ⨆ i, p i = Subsemigroup.closure (⋃ i, (p i : Set M))

Proof state:
M : Type u_1
inst✝ : Mul M
ι : Sort u_3
p : ι → Subsemigroup M
⊢ ⨆ i, p i = closure (⋃ i, ↑(p i))

Tactic:
simp_rw [Subsemigroup.closure_iUnion, Subsemigroup.closure_eq]

Result:
no goals
-- Mathlib/Data/Int/ModEq.lean
theorem modEq_iff_add_fac {a b n : ℤ} : a ≡ b [ZMOD n] ↔ ∃ t, b = a + n * t

Proof state:
a b n : ℤ
⊢ a ≡ b [ZMOD n] ↔ ∃ t, b = a + n * t

Tactic:
rw [modEq_iff_dvd]

Result:
a b n : ℤ
⊢ n ∣ b - a ↔ ∃ t, b = a + n * t

Proof state:
a b n : ℤ
⊢ n ∣ b - a ↔ ∃ t, b = a + n * t

Tactic:
exact exists_congr fun t => sub_eq_iff_eq_add'

Result:
no goals
-- Mathlib/Combinatorics/Schnirelmann.lean
/--
For any natural `n`, the Schnirelmann density multiplied by `n` is bounded by `|A ∩ {1, ..., n}|`.
Note this property fails for the natural density.
-/
lemma schnirelmannDensity_mul_le_card_filter {n : ℕ} :
    schnirelmannDensity A * n ≤ #{a ∈ Ioc 0 n | a ∈ A}

Proof state:
A : Set ℕ
inst✝ : DecidablePred fun x => x ∈ A
n : ℕ
⊢ schnirelmannDensity A * ↑n ≤ ↑(#(filter (fun a => a ∈ A) (Ioc 0 n)))

Tactic:
rcases eq_or_ne n 0 with rfl | hn

Result:
case inl
A : Set ℕ
inst✝ : DecidablePred fun x => x ∈ A
⊢ schnirelmannDensity A * ↑0 ≤ ↑(#(filter (fun a => a ∈ A) (Ioc 0 0)))

case inr
A : Set ℕ
inst✝ : DecidablePred fun x => x ∈ A
n : ℕ
hn : n ≠ 0
⊢ schnirelmannDensity A * ↑n ≤ ↑(#(filter (fun a => a ∈ A) (Ioc 0 n)))

Proof state:
case inl
A : Set ℕ
inst✝ : DecidablePred fun x => x ∈ A
⊢ schnirelmannDensity A * ↑0 ≤ ↑(#(filter (fun a => a ∈ A) (Ioc 0 0)))

Tactic:
simp

Result:
no goals

Proof state:
case inr
A : Set ℕ
inst✝ : DecidablePred fun x => x ∈ A
n : ℕ
hn : n ≠ 0
⊢ schnirelmannDensity A * ↑n ≤ ↑(#(filter (fun a => a ∈ A) (Ioc 0 n)))

Tactic:
exact (le_div_iff₀ (by positivity)).1 (schnirelmannDensity_le_div hn)

Result:
no goals

Proof state:
A : Set ℕ
inst✝ : DecidablePred fun x => x ∈ A
n : ℕ
hn : n ≠ 0
⊢ 0 < ↑n

Tactic:
positivity

Result:
no goals
-- Mathlib/MeasureTheory/VectorMeasure/WithDensity.lean
theorem withDensityᵥ_smul_eq_withDensityᵥ_withDensity' {f : α → ℝ≥0∞} {g : α → E}
    (hf : AEMeasurable f μ) (hflt : ∀ᵐ x ∂μ, f x < ∞)
    (hfg : Integrable (fun x ↦ (f x).toReal • g x) μ) :
    μ.withDensityᵥ (fun x ↦ (f x).toReal • g x) = (μ.withDensity f).withDensityᵥ g

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0∞
g : α → E
hf : AEMeasurable f μ
hflt : ∀ᵐ (x : α) ∂μ, f x < ⊤
hfg : Integrable (fun x => (f x).toReal • g x) μ
⊢ (μ.withDensityᵥ fun x => (f x).toReal • g x) = μ.withDensityᵥ ((fun x => (f x).toNNReal) • g)

Tactic:
apply congr_arg

Result:
case h
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0∞
g : α → E
hf : AEMeasurable f μ
hflt : ∀ᵐ (x : α) ∂μ, f x < ⊤
hfg : Integrable (fun x => (f x).toReal • g x) μ
⊢ (fun x => (f x).toReal • g x) = (fun x => (f x).toNNReal) • g

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0∞
g : α → E
hf : AEMeasurable f μ
hflt : ∀ᵐ (x : α) ∂μ, f x < ⊤
hfg : Integrable (fun x => (f x).toReal • g x) μ
⊢ (μ.withDensityᵥ fun x => (f x).toReal • g x) = (μ.withDensity f).withDensityᵥ g

Tactic:
rw [← withDensity_congr_ae (coe_toNNReal_ae_eq hflt),
  ← withDensityᵥ_smul_eq_withDensityᵥ_withDensity hf.ennreal_toNNReal hfg]

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0∞
g : α → E
hf : AEMeasurable f μ
hflt : ∀ᵐ (x : α) ∂μ, f x < ⊤
hfg : Integrable (fun x => (f x).toReal • g x) μ
⊢ (μ.withDensityᵥ fun x => (f x).toReal • g x) = μ.withDensityᵥ ((fun x => (f x).toNNReal) • g)

Proof state:
case h
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0∞
g : α → E
hf : AEMeasurable f μ
hflt : ∀ᵐ (x : α) ∂μ, f x < ⊤
hfg : Integrable (fun x => (f x).toReal • g x) μ
⊢ (fun x => (f x).toReal • g x) = (fun x => (f x).toNNReal) • g

Tactic:
ext

Result:
case h.h
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0∞
g : α → E
hf : AEMeasurable f μ
hflt : ∀ᵐ (x : α) ∂μ, f x < ⊤
hfg : Integrable (fun x => (f x).toReal • g x) μ
x✝ : α
⊢ (f x✝).toReal • g x✝ = ((fun x => (f x).toNNReal) • g) x✝

Proof state:
case h.h
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_2
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℝ E
f : α → ℝ≥0∞
g : α → E
hf : AEMeasurable f μ
hflt : ∀ᵐ (x : α) ∂μ, f x < ⊤
hfg : Integrable (fun x => (f x).toReal • g x) μ
x✝ : α
⊢ (f x✝).toReal • g x✝ = ((fun x => (f x).toNNReal) • g) x✝

Tactic:
simp [NNReal.smul_def, ENNReal.coe_toNNReal_eq_toReal]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/ToLin.lean
lemma Matrix.linearIndependent_rows_of_isUnit {R : Type*} [CommRing R] {A : Matrix m m R}
    [DecidableEq m] (ha : IsUnit A) : LinearIndependent R (fun i ↦ A i)

Proof state:
m : Type u_3
inst✝² : Fintype m
R : Type u_5
inst✝¹ : CommRing R
A : Matrix m m R
inst✝ : DecidableEq m
ha : IsUnit A
⊢ LinearIndependent R fun i => A i

Tactic:
rw [← Matrix.vecMul_injective_iff]

Result:
m : Type u_3
inst✝² : Fintype m
R : Type u_5
inst✝¹ : CommRing R
A : Matrix m m R
inst✝ : DecidableEq m
ha : IsUnit A
⊢ Function.Injective fun v => v ᵥ* A

Proof state:
m : Type u_3
inst✝² : Fintype m
R : Type u_5
inst✝¹ : CommRing R
A : Matrix m m R
inst✝ : DecidableEq m
ha : IsUnit A
⊢ Function.Injective fun v => v ᵥ* A

Tactic:
exact Matrix.vecMul_injective_of_isUnit ha

Result:
no goals
-- Mathlib/LinearAlgebra/BilinearForm/Orthogonal.lean
theorem isOrtho_smul_right {x y : M₄} {a : R₄} (ha : a ≠ 0) :
    IsOrtho G x (a • y) ↔ IsOrtho G x y

Proof state:
R₄ : Type u_7
M₄ : Type u_8
inst✝³ : CommRing R₄
inst✝² : IsDomain R₄
inst✝¹ : AddCommGroup M₄
inst✝ : Module R₄ M₄
G : BilinForm R₄ M₄
x y : M₄
a : R₄
ha : a ≠ 0
⊢ a = 0 → (G x) y = 0

Tactic:
exact fun a ↦ (ha a).elim

Result:
no goals

Proof state:
R₄ : Type u_7
M₄ : Type u_8
inst✝³ : CommRing R₄
inst✝² : IsDomain R₄
inst✝¹ : AddCommGroup M₄
inst✝ : Module R₄ M₄
G : BilinForm R₄ M₄
x y : M₄
a : R₄
ha : a ≠ 0
⊢ a • (G x) y = 0 ↔ (G x) y = 0

Tactic:
simp only [smul_eq_mul, mul_eq_zero, or_iff_right_iff_imp]

Result:
R₄ : Type u_7
M₄ : Type u_8
inst✝³ : CommRing R₄
inst✝² : IsDomain R₄
inst✝¹ : AddCommGroup M₄
inst✝ : Module R₄ M₄
G : BilinForm R₄ M₄
x y : M₄
a : R₄
ha : a ≠ 0
⊢ a = 0 → (G x) y = 0

Proof state:
R₄ : Type u_7
M₄ : Type u_8
inst✝³ : CommRing R₄
inst✝² : IsDomain R₄
inst✝¹ : AddCommGroup M₄
inst✝ : Module R₄ M₄
G : BilinForm R₄ M₄
x y : M₄
a : R₄
ha : a ≠ 0
⊢ (G x) (a • y) = 0 ↔ (G x) y = 0

Tactic:
rw [map_smul]

Result:
R₄ : Type u_7
M₄ : Type u_8
inst✝³ : CommRing R₄
inst✝² : IsDomain R₄
inst✝¹ : AddCommGroup M₄
inst✝ : Module R₄ M₄
G : BilinForm R₄ M₄
x y : M₄
a : R₄
ha : a ≠ 0
⊢ a • (G x) y = 0 ↔ (G x) y = 0

Proof state:
R₄ : Type u_7
M₄ : Type u_8
inst✝³ : CommRing R₄
inst✝² : IsDomain R₄
inst✝¹ : AddCommGroup M₄
inst✝ : Module R₄ M₄
G : BilinForm R₄ M₄
x y : M₄
a : R₄
ha : a ≠ 0
⊢ G.IsOrtho x (a • y) ↔ G.IsOrtho x y

Tactic:
dsimp only [IsOrtho]

Result:
R₄ : Type u_7
M₄ : Type u_8
inst✝³ : CommRing R₄
inst✝² : IsDomain R₄
inst✝¹ : AddCommGroup M₄
inst✝ : Module R₄ M₄
G : BilinForm R₄ M₄
x y : M₄
a : R₄
ha : a ≠ 0
⊢ (G x) (a • y) = 0 ↔ (G x) y = 0
-- Mathlib/Logic/Function/Basic.lean
theorem exists_update_iff (f : ∀ a, β a) {a : α} {b : β a} (p : ∀ a, β a → Prop) :
    (∃ x, p x (update f a b x)) ↔ p a b ∨ ∃ x ≠ a, p x (f x)

Proof state:
α : Sort u
β : α → Sort v
inst✝ : DecidableEq α
f : (a : α) → β a
a : α
b : β a
p : (a : α) → β a → Prop
⊢ ¬(¬p a b ∧ ∀ (x : α), x ≠ a → ¬p x (f x)) ↔ p a b ∨ ∃ x, x ≠ a ∧ p x (f x)

Tactic:
simp [-not_and, not_and_or]

Result:
no goals

Proof state:
α : Sort u
β : α → Sort v
inst✝ : DecidableEq α
f : (a : α) → β a
a : α
b : β a
p : (a : α) → β a → Prop
⊢ (∃ x, p x (update f a b x)) ↔ p a b ∨ ∃ x, x ≠ a ∧ p x (f x)

Tactic:
rw [← not_forall_not, forall_update_iff f fun a b ↦ ¬p a b]

Result:
α : Sort u
β : α → Sort v
inst✝ : DecidableEq α
f : (a : α) → β a
a : α
b : β a
p : (a : α) → β a → Prop
⊢ ¬(¬p a b ∧ ∀ (x : α), x ≠ a → ¬p x (f x)) ↔ p a b ∨ ∃ x, x ≠ a ∧ p x (f x)
-- Mathlib/Data/Ordmap/Ordset.lean
theorem toList_node (s l x r) : toList (@node α s l x r) = toList l ++ x :: toList r

Proof state:
α : Type u_1
s : ℕ
l : Ordnode α
x : α
r : Ordnode α
⊢ (node s l x r).toList = l.toList ++ x :: r.toList

Tactic:
rw [toList, foldr, foldr_cons_eq_toList]

Result:
α : Type u_1
s : ℕ
l : Ordnode α
x : α
r : Ordnode α
⊢ l.toList ++ x :: foldr List.cons r [] = l.toList ++ x :: r.toList

Proof state:
α : Type u_1
s : ℕ
l : Ordnode α
x : α
r : Ordnode α
⊢ l.toList ++ x :: foldr List.cons r [] = l.toList ++ x :: r.toList

Tactic:
rfl

Result:
no goals
-- Mathlib/MeasureTheory/Integral/CircleIntegral.lean
theorem integral_sub {f g : ℂ → E} {c : ℂ} {R : ℝ} (hf : CircleIntegrable f c R)
    (hg : CircleIntegrable g c R) :
    (∮ z in C(c, R), f z - g z) = (∮ z in C(c, R), f z) - ∮ z in C(c, R), g z

Proof state:
E : Type u_1
inst✝¹ : NormedAddCommGroup E
inst✝ : NormedSpace ℂ E
f g : ℂ → E
c : ℂ
R : ℝ
hf : CircleIntegrable f c R
hg : CircleIntegrable g c R
⊢ (∮ (z : ℂ) in C(c, R), f z - g z) = (∮ (z : ℂ) in C(c, R), f z) - ∮ (z : ℂ) in C(c, R), g z

Tactic:
simp only [circleIntegral, smul_sub, intervalIntegral.integral_sub hf.out hg.out]

Result:
no goals
-- Mathlib/Dynamics/PeriodicPts/Lemmas.lean
theorem minimalPeriod_fst_dvd : minimalPeriod f x.1 ∣ minimalPeriod (Prod.map f g) x

Proof state:
α : Type u_1
β : Type u_2
f : α → α
g : β → β
x : α × β
⊢ minimalPeriod f x.1 ∣ (minimalPeriod f x.1).lcm (minimalPeriod g x.2)

Tactic:
exact Nat.dvd_lcm_left _ _

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
f : α → α
g : β → β
x : α × β
⊢ minimalPeriod f x.1 ∣ minimalPeriod (Prod.map f g) x

Tactic:
rw [minimalPeriod_prod_map]

Result:
α : Type u_1
β : Type u_2
f : α → α
g : β → β
x : α × β
⊢ minimalPeriod f x.1 ∣ (minimalPeriod f x.1).lcm (minimalPeriod g x.2)
-- Mathlib/Logic/Function/Basic.lean
/-- A relation `r : α → β → Prop` is "function-like"
(for each `a` there exists a unique `b` such that `r a b`)
if and only if it is `(f · = ·)` for some function `f`. -/
lemma forall_existsUnique_iff' {r : α → β → Prop} :
    (∀ a, ∃! b, r a b) ↔ ∃ f : α → β, r = (f · = ·)

Proof state:
α : Sort u_1
β : Sort u_2
r : α → β → Prop
⊢ (∀ (a : α), ∃! b, r a b) ↔ ∃ f, r = fun x1 x2 => f x1 = x2

Tactic:
simp [forall_existsUnique_iff, funext_iff]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Find.lean
theorem find?_some : ∀ {l}, find? p l = some a → p a
  | b :: l, H => by
    by_cases h : p b <;> simp [find?, h] at H
    · exact H ▸ h
    · exact find?_some H

Proof state:
α✝ : Type u_1
p : α✝ → Bool
a b : α✝
l : List α✝
H : find? p (b :: l) = some a
⊢ p a = true

Tactic:
by_cases h : p b <;> simp [find?, h] at H

Result:
case pos
α✝ : Type u_1
p : α✝ → Bool
a b : α✝
l : List α✝
h : p b = true
H : b = a
⊢ p a = true

case neg
α✝ : Type u_1
p : α✝ → Bool
a b : α✝
l : List α✝
h : ¬p b = true
H : find? p l = some a
⊢ p a = true

Proof state:
case pos
α✝ : Type u_1
p : α✝ → Bool
a b : α✝
l : List α✝
h : p b = true
H : b = a
⊢ p a = true

Tactic:
exact H ▸ h

Result:
no goals

Proof state:
case neg
α✝ : Type u_1
p : α✝ → Bool
a b : α✝
l : List α✝
h : ¬p b = true
H : find? p l = some a
⊢ p a = true

Tactic:
exact find?_some H

Result:
no goals
-- Mathlib/Order/WithBot.lean
@[simp, norm_cast] lemma coe_le_coe : (a : WithTop α) ≤ b ↔ a ≤ b

Proof state:
α : Type u_1
a b : α
inst✝ : LE α
⊢ ↑a ≤ ↑b ↔ a ≤ b

Tactic:
simp [le_def]

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/Adjugate.lean
theorem cramer_is_linear : IsLinearMap α (cramerMap A)

Proof state:
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
⊢ IsLinearMap α A.cramerMap

Tactic:
constructor <;> intros <;> ext i

Result:
case map_add.h
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
x✝ y✝ : n → α
i : n
⊢ A.cramerMap (x✝ + y✝) i = (A.cramerMap x✝ + A.cramerMap y✝) i

case map_smul.h
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
c✝ : α
x✝ : n → α
i : n
⊢ A.cramerMap (c✝ • x✝) i = (c✝ • A.cramerMap x✝) i

Proof state:
case map_add.h
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
x✝ y✝ : n → α
i : n
⊢ A.cramerMap (x✝ + y✝) i = (A.cramerMap x✝ + A.cramerMap y✝) i

Tactic:
apply (cramerMap_is_linear A i).1

Result:
no goals

Proof state:
case map_smul.h
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
c✝ : α
x✝ : n → α
i : n
⊢ A.cramerMap (c✝ • x✝) i = (c✝ • A.cramerMap x✝) i

Tactic:
apply (cramerMap_is_linear A i).2

Result:
no goals
-- Mathlib/LinearAlgebra/TensorProduct/Basic.lean
theorem lift_mk_compr₂ (f : M ⊗ N →ₗ[R] P) : lift ((mk R M N).compr₂ f) = f

Proof state:
R : Type u_1
inst✝⁶ : CommSemiring R
M : Type u_5
N : Type u_6
P : Type u_7
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid N
inst✝³ : AddCommMonoid P
inst✝² : Module R M
inst✝¹ : Module R N
inst✝ : Module R P
f : M ⊗[R] N →ₗ[R] P
⊢ lift ((mk R M N).compr₂ f) = f

Tactic:
rw [lift_compr₂ f, lift_mk, LinearMap.comp_id]

Result:
no goals
-- Mathlib/Data/Set/Subset.lean
@[simp]
lemma image_val_sInter (hT : T.Nonempty) : (↑(⋂₀ T) : Set α) = ⋂₀ { (↑B : Set α) | B ∈ T }

Proof state:
α : Type u_2
A : Set α
T : Set (Set ↑A)
hT : T.Nonempty
⊢ Subtype.val '' ⋂₀ T = ⋂₀ {x | ∃ B ∈ T, Subtype.val '' B = x}

Tactic:
rw [← Set.image, sInter_image, sInter_eq_biInter, Subtype.val_injective.injOn.image_biInter_eq hT]

Result:
no goals
-- Mathlib/RingTheory/Polynomial/Chebyshev.lean
theorem C_two : C R 2 = X ^ 2 - 2

Proof state:
R : Type u_1
inst✝ : CommRing R
⊢ C R 2 = X ^ 2 - 2

Tactic:
simpa [pow_two, mul_assoc] using C_add_two R 0

Result:
no goals
-- Mathlib/CategoryTheory/Functor/Derived/RightDerived.lean
lemma isRightDerivedFunctor_iff_isIso_rightDerivedDesc (G : D ⥤ H) (β : F ⟶ L ⋙ G) :
    G.IsRightDerivedFunctor β W ↔ IsIso (RF.rightDerivedDesc α W G β)

Proof state:
C : Type u_5
D : Type u_3
H : Type u_4
inst✝⁴ : Category.{u_6, u_5} C
inst✝³ : Category.{u_1, u_3} D
inst✝² : Category.{u_2, u_4} H
RF : D ⥤ H
F : C ⥤ H
L : C ⥤ D
α : F ⟶ L ⋙ RF
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : RF.IsRightDerivedFunctor α W
G : D ⥤ H
β : F ⟶ L ⋙ G
this : RF.IsLeftKanExtension α
⊢ G.IsLeftKanExtension β ↔ IsIso (RF.rightDerivedDesc α W G β)

Tactic:
exact isLeftKanExtension_iff_isIso _ α _ (by simp)

Result:
no goals

Proof state:
C : Type u_5
D : Type u_3
H : Type u_4
inst✝⁴ : Category.{u_6, u_5} C
inst✝³ : Category.{u_1, u_3} D
inst✝² : Category.{u_2, u_4} H
RF : D ⥤ H
F : C ⥤ H
L : C ⥤ D
α : F ⟶ L ⋙ RF
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : RF.IsRightDerivedFunctor α W
G : D ⥤ H
β : F ⟶ L ⋙ G
this : RF.IsLeftKanExtension α
⊢ α ≫ whiskerLeft L (RF.rightDerivedDesc α W G β) = β

Tactic:
simp

Result:
no goals

Proof state:
C : Type u_5
D : Type u_3
H : Type u_4
inst✝⁴ : Category.{u_6, u_5} C
inst✝³ : Category.{u_1, u_3} D
inst✝² : Category.{u_2, u_4} H
RF : D ⥤ H
F : C ⥤ H
L : C ⥤ D
α : F ⟶ L ⋙ RF
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : RF.IsRightDerivedFunctor α W
G : D ⥤ H
β : F ⟶ L ⋙ G
⊢ G.IsLeftKanExtension β ↔ IsIso (RF.rightDerivedDesc α W G β)

Tactic:
have := IsRightDerivedFunctor.isLeftKanExtension _ α W

Result:
C : Type u_5
D : Type u_3
H : Type u_4
inst✝⁴ : Category.{u_6, u_5} C
inst✝³ : Category.{u_1, u_3} D
inst✝² : Category.{u_2, u_4} H
RF : D ⥤ H
F : C ⥤ H
L : C ⥤ D
α : F ⟶ L ⋙ RF
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : RF.IsRightDerivedFunctor α W
G : D ⥤ H
β : F ⟶ L ⋙ G
this : RF.IsLeftKanExtension α
⊢ G.IsLeftKanExtension β ↔ IsIso (RF.rightDerivedDesc α W G β)

Proof state:
C : Type u_5
D : Type u_3
H : Type u_4
inst✝⁴ : Category.{u_6, u_5} C
inst✝³ : Category.{u_1, u_3} D
inst✝² : Category.{u_2, u_4} H
RF : D ⥤ H
F : C ⥤ H
L : C ⥤ D
α : F ⟶ L ⋙ RF
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : RF.IsRightDerivedFunctor α W
G : D ⥤ H
β : F ⟶ L ⋙ G
⊢ G.IsRightDerivedFunctor β W ↔ IsIso (RF.rightDerivedDesc α W G β)

Tactic:
rw [isRightDerivedFunctor_iff_isLeftKanExtension]

Result:
C : Type u_5
D : Type u_3
H : Type u_4
inst✝⁴ : Category.{u_6, u_5} C
inst✝³ : Category.{u_1, u_3} D
inst✝² : Category.{u_2, u_4} H
RF : D ⥤ H
F : C ⥤ H
L : C ⥤ D
α : F ⟶ L ⋙ RF
W : MorphismProperty C
inst✝¹ : L.IsLocalization W
inst✝ : RF.IsRightDerivedFunctor α W
G : D ⥤ H
β : F ⟶ L ⋙ G
⊢ G.IsLeftKanExtension β ↔ IsIso (RF.rightDerivedDesc α W G β)