harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Data/Multiset/ZeroCons.lean
theorem Rel.mono {r p : α → β → Prop} {s t} (hst : Rel r s t)
    (h : ∀ a ∈ s, ∀ b ∈ t, r a b → p a b) : Rel p s t

Proof state:
case cons
α : Type u_1
β : Type v
r p : α → β → Prop
s✝ : Multiset α
t✝ : Multiset β
a : α
b : β
s : Multiset α
t : Multiset β
hab : r a b
_hst : Rel r s t
ih : (∀ (a : α), a ∈ s → ∀ (b : β), b ∈ t → r a b → p a b) → Rel p s t
h : ∀ (a_1 : α), a_1 ∈ a ::ₘ s → ∀ (b_1 : β), b_1 ∈ b ::ₘ t → r a_1 b_1 → p a_1 b_1
⊢ Rel p s t

Tactic:
exact ih fun a' ha' b' hb' h' => h a' (mem_cons_of_mem ha') b' (mem_cons_of_mem hb') h'

Result:
no goals

Proof state:
case zero
α : Type u_1
β : Type v
r p : α → β → Prop
s : Multiset α
t : Multiset β
h : ∀ (a : α), a ∈ 0 → ∀ (b : β), b ∈ 0 → r a b → p a b
⊢ Rel p 0 0

Tactic:
exact Rel.zero

Result:
no goals

Proof state:
case cons
α : Type u_1
β : Type v
r p : α → β → Prop
s✝ : Multiset α
t✝ : Multiset β
a : α
b : β
s : Multiset α
t : Multiset β
hab : r a b
_hst : Rel r s t
ih : (∀ (a : α), a ∈ s → ∀ (b : β), b ∈ t → r a b → p a b) → Rel p s t
h : ∀ (a_1 : α), a_1 ∈ a ::ₘ s → ∀ (b_1 : β), b_1 ∈ b ::ₘ t → r a_1 b_1 → p a_1 b_1
⊢ Rel p (a ::ₘ s) (b ::ₘ t)

Tactic:
apply Rel.cons (h a (mem_cons_self _ _) b (mem_cons_self _ _) hab)

Result:
case cons
α : Type u_1
β : Type v
r p : α → β → Prop
s✝ : Multiset α
t✝ : Multiset β
a : α
b : β
s : Multiset α
t : Multiset β
hab : r a b
_hst : Rel r s t
ih : (∀ (a : α), a ∈ s → ∀ (b : β), b ∈ t → r a b → p a b) → Rel p s t
h : ∀ (a_1 : α), a_1 ∈ a ::ₘ s → ∀ (b_1 : β), b_1 ∈ b ::ₘ t → r a_1 b_1 → p a_1 b_1
⊢ Rel p s t

Proof state:
α : Type u_1
β : Type v
r p : α → β → Prop
s : Multiset α
t : Multiset β
hst : Rel r s t
h : ∀ (a : α), a ∈ s → ∀ (b : β), b ∈ t → r a b → p a b
⊢ Rel p s t

Tactic:
induction hst with
| zero => exact Rel.zero
| @cons a b s t hab _hst ih =>
  apply Rel.cons (h a (mem_cons_self _ _) b (mem_cons_self _ _) hab)
  exact ih fun a' ha' b' hb' h' => h a' (mem_cons_of_mem ha') b' (mem_cons_of_mem hb') h'

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem getElem_of_mem {a} {l : Array α} (h : a ∈ l) : ∃ (i : Nat) (h : i < l.size), l[i]'h = a

Proof state:
α : Type u_1
a : α
toList✝ : List α
h : a ∈ { toList := toList✝ }
⊢ ?m.39835 ∈ ?m.39836

Tactic:
simpa using h

Result:
no goals

Proof state:
case mk
α : Type u_1
a : α
toList✝ : List α
h : a ∈ { toList := toList✝ }
⊢ ∃ i h, { toList := toList✝ }[i] = a

Tactic:
simp [List.getElem_of_mem (by simpa using h)]

Result:
no goals

Proof state:
α : Type u_1
a : α
l : Array α
h : a ∈ l
⊢ ∃ i h, l[i] = a

Tactic:
cases l

Result:
case mk
α : Type u_1
a : α
toList✝ : List α
h : a ∈ { toList := toList✝ }
⊢ ∃ i h, { toList := toList✝ }[i] = a
-- Mathlib/Order/Interval/Set/OrdConnectedComponent.lean
theorem dual_ordSeparatingSet :
    ordSeparatingSet (ofDual ⁻¹' s) (ofDual ⁻¹' t) = ofDual ⁻¹' ordSeparatingSet s t

Proof state:
α : Type u_1
inst✝ : LinearOrder α
s t : Set α
⊢ (⇑ofDual ⁻¹' s).ordSeparatingSet (⇑ofDual ⁻¹' t) = ⇑ofDual ⁻¹' s.ordSeparatingSet t

Tactic:
simp only [ordSeparatingSet, mem_preimage, ← toDual.surjective.iUnion_comp, ofDual_toDual,
  dual_ordConnectedComponent, ← preimage_compl, preimage_inter, preimage_iUnion]

Result:
no goals
-- Mathlib/GroupTheory/OreLocalization/Basic.lean
theorem oreDiv_smul_char (r₁ : R) (r₂ : X) (s₁ s₂ : S) (r' : R) (s' : S) (huv : s' * r₁ = r' * s₂) :
    (r₁ /ₒ s₁) • (r₂ /ₒ s₂) = r' • r₂ /ₒ (s' * s₁)

Proof state:
R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type u_2
inst✝ : MulAction R X
r₁ : R
r₂ : X
s₁ s₂ : ↥S
r' : R
s' : ↥S
huv : ↑s' * r₁ = r' * ↑s₂
⊢ (r₁ /ₒ s₁) • (r₂ /ₒ s₂) = r' • r₂ /ₒ (s' * s₁)

Tactic:
with_unfolding_all exact smul'_char r₁ r₂ s₁ s₂ s' r' huv

Result:
no goals

Proof state:
R : Type u_1
inst✝² : Monoid R
S : Submonoid R
inst✝¹ : OreSet S
X : Type u_2
inst✝ : MulAction R X
r₁ : R
r₂ : X
s₁ s₂ : ↥S
r' : R
s' : ↥S
huv : ↑s' * r₁ = r' * ↑s₂
⊢ (r₁ /ₒ s₁) • (r₂ /ₒ s₂) = r' • r₂ /ₒ (s' * s₁)

Tactic:
exact smul'_char r₁ r₂ s₁ s₂ s' r' huv

Result:
no goals
-- Mathlib/SetTheory/Surreal/Basic.lean
/-- A small set of surreals is bounded above. -/
lemma bddAbove_of_small (s : Set Surreal.{u}) [Small.{u} s] : BddAbove s

Proof state:
s : Set Surreal
inst✝ : Small.{u, u + 1} ↑s
⊢ BddAbove s

Tactic:
simpa using bddAbove_range_of_small (Subtype.val : s → Surreal.{u})

Result:
no goals
-- Mathlib/Topology/Maps/Basic.lean
lemma isClosed_iff_preimage_isClosed (hf : IsClosedEmbedding f) {s : Set Y}
    (hs : s ⊆ range f) : IsClosed s ↔ IsClosed (f ⁻¹' s)

Proof state:
X : Type u_1
Y : Type u_2
f : X → Y
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
hf : IsClosedEmbedding f
s : Set Y
hs : s ⊆ range f
⊢ IsClosed s ↔ IsClosed (f ⁻¹' s)

Tactic:
rw [hf.isClosed_iff_image_isClosed, image_preimage_eq_of_subset hs]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Lemmas.lean
theorem max_lt {a b c : Nat} : max a b < c ↔ a < c ∧ b < c

Proof state:
a b c : Nat
⊢ max a b < c ↔ a < c ∧ b < c

Tactic:
rw [← Nat.succ_le, ← Nat.succ_max_succ a b]

Result:
a b c : Nat
⊢ max a.succ b.succ ≤ c ↔ a < c ∧ b < c

Proof state:
a b c : Nat
⊢ max a.succ b.succ ≤ c ↔ a < c ∧ b < c

Tactic:
exact Nat.max_le

Result:
no goals
-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Unique.lean
lemma realContinuousMapOfNNReal_injective :
    Function.Injective (realContinuousMapOfNNReal (X := X) (A := A))

Proof state:
case h
X : Type u_1
inst✝³ : TopologicalSpace X
A : Type u_2
inst✝² : Ring A
inst✝¹ : StarRing A
inst✝ : Algebra ℝ A
φ ψ : C(X, ℝ≥0) →⋆ₐ[ℝ≥0] A
h : φ.realContinuousMapOfNNReal = ψ.realContinuousMapOfNNReal
f : C(X, ℝ≥0)
⊢ φ f = ψ f

Tactic:
simpa using congr($(h) ((ContinuousMap.mk toReal continuous_coe).comp f))

Result:
no goals

Proof state:
X : Type u_1
inst✝³ : TopologicalSpace X
A : Type u_2
inst✝² : Ring A
inst✝¹ : StarRing A
inst✝ : Algebra ℝ A
φ ψ : C(X, ℝ≥0) →⋆ₐ[ℝ≥0] A
h : φ.realContinuousMapOfNNReal = ψ.realContinuousMapOfNNReal
⊢ φ = ψ

Tactic:
ext f

Result:
case h
X : Type u_1
inst✝³ : TopologicalSpace X
A : Type u_2
inst✝² : Ring A
inst✝¹ : StarRing A
inst✝ : Algebra ℝ A
φ ψ : C(X, ℝ≥0) →⋆ₐ[ℝ≥0] A
h : φ.realContinuousMapOfNNReal = ψ.realContinuousMapOfNNReal
f : C(X, ℝ≥0)
⊢ φ f = ψ f

Proof state:
X : Type u_1
inst✝³ : TopologicalSpace X
A : Type u_2
inst✝² : Ring A
inst✝¹ : StarRing A
inst✝ : Algebra ℝ A
⊢ Function.Injective realContinuousMapOfNNReal

Tactic:
intro φ ψ h

Result:
X : Type u_1
inst✝³ : TopologicalSpace X
A : Type u_2
inst✝² : Ring A
inst✝¹ : StarRing A
inst✝ : Algebra ℝ A
φ ψ : C(X, ℝ≥0) →⋆ₐ[ℝ≥0] A
h : φ.realContinuousMapOfNNReal = ψ.realContinuousMapOfNNReal
⊢ φ = ψ
-- Mathlib/Order/CompleteLattice.lean
theorem iSup_prod {f : β × γ → α} : ⨆ x, f x = ⨆ (i) (j), f (i, j) :=
  eq_of_forall_ge_iff fun c => by simp only [iSup_le_iff, Prod.forall]

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
inst✝ : CompleteLattice α
f : β × γ → α
c : α
⊢ ⨆ x, f x ≤ c ↔ ⨆ i, ⨆ j, f (i, j) ≤ c

Tactic:
simp only [iSup_le_iff, Prod.forall]

Result:
no goals
-- Mathlib/CategoryTheory/MorphismProperty/Composition.lean
lemma multiplicativeClosure_monotone :
    Monotone (multiplicativeClosure (C := C)) :=
  fun _ W' h ↦ by simpa using h.trans W'.le_multiplicativeClosure

Proof state:
C : Type u
inst✝ : Category.{v, u} C
x✝ W' : MorphismProperty C
h : x✝ ≤ W'
⊢ x✝.multiplicativeClosure ≤ W'.multiplicativeClosure

Tactic:
simpa using h.trans W'.le_multiplicativeClosure

Result:
no goals
-- Mathlib/RingTheory/FractionalIdeal/Operations.lean
theorem isNoetherian [IsNoetherianRing R₁] (I : FractionalIdeal R₁⁰ K) : IsNoetherian R₁ I

Proof state:
case intro.intro.intro
R₁ : Type u_3
inst✝⁵ : CommRing R₁
K : Type u_4
inst✝⁴ : Field K
inst✝³ : Algebra R₁ K
inst✝² : IsFractionRing R₁ K
inst✝¹ : IsDomain R₁
inst✝ : IsNoetherianRing R₁
d : R₁
J : Ideal R₁
left✝ : d ≠ 0
⊢ IsNoetherian R₁ ↥↑(spanSingleton R₁⁰ ((algebraMap R₁ K) d)⁻¹ * ↑J)

Tactic:
apply isNoetherian_spanSingleton_inv_to_map_mul

Result:
case intro.intro.intro.hI
R₁ : Type u_3
inst✝⁵ : CommRing R₁
K : Type u_4
inst✝⁴ : Field K
inst✝³ : Algebra R₁ K
inst✝² : IsFractionRing R₁ K
inst✝¹ : IsDomain R₁
inst✝ : IsNoetherianRing R₁
d : R₁
J : Ideal R₁
left✝ : d ≠ 0
⊢ IsNoetherian R₁ ↥↑↑J

Proof state:
R₁ : Type u_3
inst✝⁵ : CommRing R₁
K : Type u_4
inst✝⁴ : Field K
inst✝³ : Algebra R₁ K
inst✝² : IsFractionRing R₁ K
inst✝¹ : IsDomain R₁
inst✝ : IsNoetherianRing R₁
I : FractionalIdeal R₁⁰ K
⊢ IsNoetherian R₁ ↥↑I

Tactic:
obtain ⟨d, J, _, rfl⟩ := exists_eq_spanSingleton_mul I

Result:
case intro.intro.intro
R₁ : Type u_3
inst✝⁵ : CommRing R₁
K : Type u_4
inst✝⁴ : Field K
inst✝³ : Algebra R₁ K
inst✝² : IsFractionRing R₁ K
inst✝¹ : IsDomain R₁
inst✝ : IsNoetherianRing R₁
d : R₁
J : Ideal R₁
left✝ : d ≠ 0
⊢ IsNoetherian R₁ ↥↑(spanSingleton R₁⁰ ((algebraMap R₁ K) d)⁻¹ * ↑J)

Proof state:
case intro.intro.intro.hI
R₁ : Type u_3
inst✝⁵ : CommRing R₁
K : Type u_4
inst✝⁴ : Field K
inst✝³ : Algebra R₁ K
inst✝² : IsFractionRing R₁ K
inst✝¹ : IsDomain R₁
inst✝ : IsNoetherianRing R₁
d : R₁
J : Ideal R₁
left✝ : d ≠ 0
⊢ IsNoetherian R₁ ↥↑↑J

Tactic:
apply isNoetherian_coeIdeal

Result:
no goals
-- Mathlib/CategoryTheory/MorphismProperty/Limits.lean
lemma pushouts_monotone : Monotone (pushouts (C := C))

Proof state:
C : Type u
inst✝ : Category.{v, u} C
⊢ Monotone pushouts

Tactic:
rintro _ _ h _ _ _ ⟨_, _, _, _, _, hp, sq⟩

Result:
case intro.intro.intro.intro.intro.intro
C : Type u
inst✝ : Category.{v, u} C
a✝ b✝ : MorphismProperty C
h : a✝ ≤ b✝
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
w✝⁴ w✝³ : C
w✝² : w✝⁴ ⟶ w✝³
w✝¹ : w✝⁴ ⟶ X✝
w✝ : w✝³ ⟶ Y✝
hp : a✝ w✝²
sq : IsPushout w✝¹ w✝² f✝ w✝
⊢ b✝.pushouts f✝

Proof state:
case intro.intro.intro.intro.intro.intro
C : Type u
inst✝ : Category.{v, u} C
a✝ b✝ : MorphismProperty C
h : a✝ ≤ b✝
X✝ Y✝ : C
f✝ : X✝ ⟶ Y✝
w✝⁴ w✝³ : C
w✝² : w✝⁴ ⟶ w✝³
w✝¹ : w✝⁴ ⟶ X✝
w✝ : w✝³ ⟶ Y✝
hp : a✝ w✝²
sq : IsPushout w✝¹ w✝² f✝ w✝
⊢ b✝.pushouts f✝

Tactic:
exact ⟨_, _, _, _, _, h _ hp, sq⟩

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/SchurComplement.lean
theorem isUnit_fromBlocks_iff_of_invertible₂₂ {A : Matrix m m α} {B : Matrix m n α}
    {C : Matrix n m α} {D : Matrix n n α} [Invertible D] :
    IsUnit (fromBlocks A B C D) ↔ IsUnit (A - B * ⅟ D * C)

Proof state:
m : Type u_2
n : Type u_3
α : Type u_4
inst✝⁵ : Fintype m
inst✝⁴ : Fintype n
inst✝³ : DecidableEq m
inst✝² : DecidableEq n
inst✝¹ : CommRing α
A : Matrix m m α
B : Matrix m n α
C : Matrix n m α
D : Matrix n n α
inst✝ : Invertible D
⊢ IsUnit (fromBlocks A B C D) ↔ IsUnit (A - B * ⅟D * C)

Tactic:
simp only [← nonempty_invertible_iff_isUnit,
  (invertibleEquivFromBlocks₂₂Invertible A B C D).nonempty_congr]

Result:
no goals
-- Mathlib/Data/Fin/Tuple/Take.lean
theorem get_take_eq_take_get_comp_cast {α : Type*} {m : ℕ} (l : List α) (h : m ≤ l.length) :
    (l.take m).get = take m h l.get ∘ Fin.cast (List.length_take_of_le h)

Proof state:
case h
α : Type u_2
m : ℕ
l : List α
h : m ≤ l.length
i : Fin (List.take m l).length
⊢ (List.take m l).get i = (take m h l.get ∘ Fin.cast ⋯) i

Tactic:
simp only [List.get_eq_getElem, List.getElem_take, comp_apply, take_apply, coe_castLE, coe_cast]

Result:
no goals

Proof state:
α : Type u_2
m : ℕ
l : List α
h : m ≤ l.length
⊢ (List.take m l).get = take m h l.get ∘ Fin.cast ⋯

Tactic:
ext i

Result:
case h
α : Type u_2
m : ℕ
l : List α
h : m ≤ l.length
i : Fin (List.take m l).length
⊢ (List.take m l).get i = (take m h l.get ∘ Fin.cast ⋯) i
-- Mathlib/Topology/MetricSpace/Pseudo/Constructions.lean
@[simp]
lemma NNReal.nndist_zero_eq_val (z : ℝ≥0) : nndist 0 z = z

Proof state:
z : ℝ≥0
⊢ nndist 0 z = z

Tactic:
simp only [NNReal.nndist_eq, max_eq_right, tsub_zero, zero_tsub, zero_le']

Result:
no goals
-- Mathlib/Analysis/Analytic/CPolynomialDef.lean
theorem FormalMultilinearSeries.continuousOn_of_finite
    (p : FormalMultilinearSeries 𝕜 E F) {n : ℕ} (hn : ∀ m, n ≤ m → p m = 0) :
    Continuous p.sum

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → p m = 0
⊢ Continuous p.sum

Tactic:
rw [continuous_iff_continuousOn_univ, ← Metric.emetric_ball_top]

Result:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → p m = 0
⊢ ContinuousOn p.sum (EMetric.ball ?m.335939 ⊤)

𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → p m = 0
⊢ E

Proof state:
𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → p m = 0
⊢ ContinuousOn p.sum (EMetric.ball ?m.335939 ⊤)

𝕜 : Type u_1
E : Type u_2
F : Type u_3
inst✝⁴ : NontriviallyNormedField 𝕜
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
inst✝¹ : NormedAddCommGroup F
inst✝ : NormedSpace 𝕜 F
p : FormalMultilinearSeries 𝕜 E F
n : ℕ
hn : ∀ (m : ℕ), n ≤ m → p m = 0
⊢ E

Tactic:
exact (p.hasFiniteFPowerSeriesOnBall_of_finite hn).continuousOn

Result:
no goals
-- Mathlib/FieldTheory/IntermediateField/Adjoin/Basic.lean
theorem finrank_eq_one_iff : finrank F K = 1 ↔ K = ⊥

Proof state:
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
K : IntermediateField F E
⊢ finrank F ↥K = 1 ↔ K = ⊥

Tactic:
rw [← toSubalgebra_inj, ← finrank_eq_finrank_subalgebra, Subalgebra.finrank_eq_one_iff,
  bot_toSubalgebra]

Result:
no goals
-- Mathlib/SetTheory/Game/Nim.lean
theorem grundyValue_neg (G : PGame) [G.Impartial] : grundyValue (-G) = grundyValue G

Proof state:
G : PGame
inst✝ : G.Impartial
⊢ (-G).grundyValue = G.grundyValue

Tactic:
rw [grundyValue_eq_iff_equiv_nim, neg_equiv_iff, neg_nim, ← grundyValue_eq_iff_equiv_nim]

Result:
no goals
-- Mathlib/Algebra/GeomSum.lean
theorem sub_one_dvd_pow_sub_one [Ring α] (x : α) (n : ℕ) :
    x - 1 ∣ x ^ n - 1

Proof state:
α : Type u
inst✝ : Ring α
x : α
n : ℕ
⊢ x - 1 ∣ x ^ n - 1 ^ n

Tactic:
exact (Commute.one_right x).sub_dvd_pow_sub_pow n

Result:
no goals

Proof state:
α : Type u
inst✝ : Ring α
x : α
n : ℕ
⊢ x - 1 ∣ x ^ n - 1

Tactic:
conv_rhs => rw [← one_pow n]

Result:
α : Type u
inst✝ : Ring α
x : α
n : ℕ
⊢ x - 1 ∣ x ^ n - 1 ^ n
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem foldl_map (f : β₁ → β₂) (g : α → β₂ → α) (l : List β₁) (init : α) :
    (l.map f).foldl g init = l.foldl (fun x y => g x (f y)) init

Proof state:
β₁ : Type u_1
β₂ : Type u_2
α : Type u_3
f : β₁ → β₂
g : α → β₂ → α
l : List β₁
init : α
⊢ foldl g init (map f l) = foldl (fun x y => g x (f y)) init l

Tactic:
induction l generalizing init <;> simp [*]

Result:
no goals
-- Mathlib/RingTheory/PrincipalIdealDomain.lean
theorem Submodule.IsPrincipal.of_comap (f : M →ₗ[R] N) (hf : Function.Surjective f)
    (S : Submodule R N) [hI : IsPrincipal (S.comap f)] : IsPrincipal S

Proof state:
R : Type u
M : Type v
N : Type u_2
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
f : M →ₗ[R] N
hf : Surjective ⇑f
S : Submodule R N
hI : (comap f S).IsPrincipal
⊢ S.IsPrincipal

Tactic:
rw [← Submodule.map_comap_eq_of_surjective hf S]

Result:
R : Type u
M : Type v
N : Type u_2
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
f : M →ₗ[R] N
hf : Surjective ⇑f
S : Submodule R N
hI : (comap f S).IsPrincipal
⊢ (Submodule.map f (comap f S)).IsPrincipal

Proof state:
R : Type u
M : Type v
N : Type u_2
inst✝⁴ : Ring R
inst✝³ : AddCommGroup M
inst✝² : AddCommGroup N
inst✝¹ : Module R M
inst✝ : Module R N
f : M →ₗ[R] N
hf : Surjective ⇑f
S : Submodule R N
hI : (comap f S).IsPrincipal
⊢ (Submodule.map f (comap f S)).IsPrincipal

Tactic:
exact hI.map f

Result:
no goals
-- Mathlib/Data/List/Basic.lean
theorem forall_map_iff {p : β → Prop} (f : α → β) : Forall p (l.map f) ↔ Forall (p ∘ f) l

Proof state:
α : Type u
β : Type v
l : List α
p : β → Prop
f : α → β
⊢ Forall p (map f l) ↔ Forall (p ∘ f) l

Tactic:
induction l <;> simp [*]

Result:
no goals
-- Mathlib/RingTheory/Polynomial/Quotient.lean
theorem quotient_map_C_eq_zero {I : Ideal R} {i : R} (hi : i ∈ I) :
    (Ideal.Quotient.mk (Ideal.map (C : R →+* MvPolynomial σ R) I :
      Ideal (MvPolynomial σ R))).comp C i = 0

Proof state:
R : Type u_1
σ : Type u_2
inst✝ : CommRing R
I : Ideal R
i : R
hi : i ∈ I
⊢ ((Ideal.Quotient.mk (Ideal.map C I)).comp C) i = 0

Tactic:
simp only [Function.comp_apply, RingHom.coe_comp, Ideal.Quotient.eq_zero_iff_mem]

Result:
R : Type u_1
σ : Type u_2
inst✝ : CommRing R
I : Ideal R
i : R
hi : i ∈ I
⊢ C i ∈ Ideal.map C I

Proof state:
R : Type u_1
σ : Type u_2
inst✝ : CommRing R
I : Ideal R
i : R
hi : i ∈ I
⊢ C i ∈ Ideal.map C I

Tactic:
exact Ideal.mem_map_of_mem _ hi

Result:
no goals
-- Mathlib/Probability/Kernel/Composition/IntegralCompProd.lean
theorem setIntegral_compProd_univ_right (f : β × γ → E) {s : Set β} (hs : MeasurableSet s)
    (hf : IntegrableOn f (s ×ˢ univ) ((κ ⊗ₖ η) a)) :
    ∫ z in s ×ˢ univ, f z ∂(κ ⊗ₖ η) a = ∫ x in s, ∫ y, f (x, y) ∂η (a, x) ∂κ a

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
E : Type u_4
mα : MeasurableSpace α
mβ : MeasurableSpace β
mγ : MeasurableSpace γ
inst✝³ : NormedAddCommGroup E
a : α
κ : Kernel α β
inst✝² : IsSFiniteKernel κ
η : Kernel (α × β) γ
inst✝¹ : IsSFiniteKernel η
inst✝ : NormedSpace ℝ E
f : β × γ → E
s : Set β
hs : MeasurableSet s
hf : IntegrableOn f (s ×ˢ univ) ((κ ⊗ₖ η) a)
⊢ ∫ (z : β × γ) in s ×ˢ univ, f z ∂(κ ⊗ₖ η) a = ∫ (x : β) in s, ∫ (y : γ), f (x, y) ∂η (a, x) ∂κ a

Tactic:
simp_rw [setIntegral_compProd hs MeasurableSet.univ hf, Measure.restrict_univ]

Result:
no goals
-- Mathlib/MeasureTheory/Function/LpSeminorm/Basic.lean
theorem memLp_const_iff {p : ℝ≥0∞} {c : E} (hp_ne_zero : p ≠ 0) (hp_ne_top : p ≠ ∞) :
    MemLp (fun _ : α => c) p μ ↔ c = 0 ∨ μ Set.univ < ∞

Proof state:
α : Type u_1
E : Type u_3
m0 : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
c : E
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
⊢ MemLp (fun x => c) p μ ↔ c = 0 ∨ μ Set.univ < ⊤

Tactic:
rw [← eLpNorm_const_lt_top_iff hp_ne_zero hp_ne_top]

Result:
α : Type u_1
E : Type u_3
m0 : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
c : E
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
⊢ MemLp (fun x => c) p μ ↔ eLpNorm (fun x => c) p μ < ⊤

Proof state:
α : Type u_1
E : Type u_3
m0 : MeasurableSpace α
μ : Measure α
inst✝ : NormedAddCommGroup E
p : ℝ≥0∞
c : E
hp_ne_zero : p ≠ 0
hp_ne_top : p ≠ ⊤
⊢ MemLp (fun x => c) p μ ↔ eLpNorm (fun x => c) p μ < ⊤

Tactic:
exact ⟨fun h => h.2, fun h => ⟨aestronglyMeasurable_const, h⟩⟩

Result:
no goals
-- Mathlib/RingTheory/Binomial.lean
theorem multichoose_two (k : ℕ) : multichoose (2 : R) k = k + 1

Proof state:
R : Type u_2
inst✝³ : NonAssocSemiring R
inst✝² : Pow R ℕ
inst✝¹ : NatPowAssoc R
inst✝ : BinomialRing R
k : ℕ
⊢ multichoose 2 k = ↑k + 1

Tactic:
induction k with
| zero =>
  rw [multichoose_zero_right, Nat.cast_zero, zero_add]
| succ n ih =>
  rw [one_add_one_eq_two.symm, multichoose_succ_succ, multichoose_one, one_add_one_eq_two, ih,
    Nat.cast_succ, add_comm]

Result:
no goals

Proof state:
case zero
R : Type u_2
inst✝³ : NonAssocSemiring R
inst✝² : Pow R ℕ
inst✝¹ : NatPowAssoc R
inst✝ : BinomialRing R
⊢ multichoose 2 0 = ↑0 + 1

Tactic:
rw [multichoose_zero_right, Nat.cast_zero, zero_add]

Result:
no goals

Proof state:
case succ
R : Type u_2
inst✝³ : NonAssocSemiring R
inst✝² : Pow R ℕ
inst✝¹ : NatPowAssoc R
inst✝ : BinomialRing R
n : ℕ
ih : multichoose 2 n = ↑n + 1
⊢ multichoose 2 (n + 1) = ↑(n + 1) + 1

Tactic:
rw [one_add_one_eq_two.symm, multichoose_succ_succ, multichoose_one, one_add_one_eq_two, ih,
  Nat.cast_succ, add_comm]

Result:
no goals
-- Mathlib/Computability/Primrec.lean
theorem encode_iff {f : α → σ} : (Primrec fun a => encode (f a)) ↔ Primrec f :=
  ⟨fun h => Nat.Primrec.of_eq h fun n => by cases @decode α _ n <;> rfl, Primrec.encode.comp⟩

Proof state:
α : Type u_1
σ : Type u_3
inst✝¹ : Primcodable α
inst✝ : Primcodable σ
f : α → σ
h : Primrec fun a => encode (f a)
n : ℕ
⊢ encode (Option.map (fun a => encode (f a)) (decode n)) = encode (Option.map f (decode n))

Tactic:
cases @decode α _ n <;> rfl

Result:
no goals
-- Mathlib/LinearAlgebra/TensorProduct/Subalgebra.lean
theorem mulMap_map_comp_eq (f : S →ₐ[R] T) :
    (mulMap (A.map f) (B.map f)).comp
      (Algebra.TensorProduct.map (f.subalgebraMap A) (f.subalgebraMap B))
        = f.comp (mulMap A B)

Proof state:
R : Type u_1
S : Type u_2
T : Type u_3
inst✝⁴ : CommSemiring R
inst✝³ : CommSemiring S
inst✝² : Algebra R S
inst✝¹ : CommSemiring T
inst✝ : Algebra R T
A B : Subalgebra R S
f : S →ₐ[R] T
⊢ ((map f A).mulMap (map f B)).comp (Algebra.TensorProduct.map (AlgHom.subalgebraMap A f) (AlgHom.subalgebraMap B f)) =
    f.comp (A.mulMap B)

Tactic:
ext <;> simp

Result:
no goals
-- Mathlib/Probability/Distributions/Gaussian.lean
theorem cgf_gaussianReal (hX : p.map X = gaussianReal μ v) (t : ℝ) :
    cgf X p t = μ * t + v * t ^ 2 / 2

Proof state:
Ω : Type u_1
mΩ : MeasurableSpace Ω
p : Measure Ω
μ : ℝ
v : ℝ≥0
X : Ω → ℝ
hX : Measure.map X p = gaussianReal μ v
t : ℝ
⊢ cgf X p t = μ * t + ↑v * t ^ 2 / 2

Tactic:
rw [cgf, mgf_gaussianReal hX t, log_exp]

Result:
no goals
-- Mathlib/Algebra/Homology/HomologicalComplexBiprod.lean
@[reassoc (attr := simp)]
lemma biprod_inr_fst_f (i : ι) :
    (biprod.inr : L ⟶ K ⊞ L).f i ≫ (biprod.fst : K ⊞ L ⟶ K).f i = 0

Proof state:
C : Type u_1
ι : Type u_2
inst✝² : Category.{u_3, u_1} C
inst✝¹ : Preadditive C
c : ComplexShape ι
K L : HomologicalComplex C c
inst✝ : ∀ (i : ι), HasBinaryBiproduct (K.X i) (L.X i)
i : ι
⊢ biprod.inr.f i ≫ biprod.fst.f i = 0

Tactic:
rw [← comp_f, biprod.inr_fst, zero_f]

Result:
no goals
-- Mathlib/Algebra/Lie/Weights/Killing.lean
@[simp]
lemma iInf_ker_weight_eq_bot :
    ⨅ α : Weight K H L, α.ker = ⊥

Proof state:
K : Type u_2
L : Type u_3
inst✝⁶ : LieRing L
inst✝⁵ : Field K
inst✝⁴ : LieAlgebra K L
inst✝³ : FiniteDimensional K L
H : LieSubalgebra K L
inst✝² : H.IsCartanSubalgebra
inst✝¹ : IsKilling K L
inst✝ : IsTriangularizable K (↥H) L
⊢ ⨅ α, Weight.ker = ⊥

Tactic:
rw [← Subspace.dualAnnihilator_inj, Subspace.dualAnnihilator_iInf_eq,
  Submodule.dualAnnihilator_bot]

Result:
K : Type u_2
L : Type u_3
inst✝⁶ : LieRing L
inst✝⁵ : Field K
inst✝⁴ : LieAlgebra K L
inst✝³ : FiniteDimensional K L
H : LieSubalgebra K L
inst✝² : H.IsCartanSubalgebra
inst✝¹ : IsKilling K L
inst✝ : IsTriangularizable K (↥H) L
⊢ ⨆ i, Weight.ker.dualAnnihilator = ⊤

Proof state:
K : Type u_2
L : Type u_3
inst✝⁶ : LieRing L
inst✝⁵ : Field K
inst✝⁴ : LieAlgebra K L
inst✝³ : FiniteDimensional K L
H : LieSubalgebra K L
inst✝² : H.IsCartanSubalgebra
inst✝¹ : IsKilling K L
inst✝ : IsTriangularizable K (↥H) L
⊢ ⨆ i, Weight.ker.dualAnnihilator = ⊤

Tactic:
simp [← LinearMap.range_dualMap_eq_dualAnnihilator_ker, ← Submodule.span_range_eq_iSup]

Result:
no goals
-- Mathlib/RingTheory/Ideal/Cotangent.lean
lemma mk_mem_cotangentIdeal {I : Ideal R} {x : R} :
    Quotient.mk (I ^ 2) x ∈ I.cotangentIdeal ↔ x ∈ I

Proof state:
R : Type u
inst✝ : CommRing R
I : Ideal R
x : R
⊢ (Quotient.mk (I ^ 2)) x ∈ I.cotangentIdeal ↔ x ∈ I

Tactic:
refine ⟨fun ⟨y, hy, e⟩ ↦ ?_,  fun h ↦ ⟨x, h, rfl⟩⟩

Result:
R : Type u
inst✝ : CommRing R
I : Ideal R
x : R
x✝ : (Quotient.mk (I ^ 2)) x ∈ I.cotangentIdeal
y : R
hy : y ∈ ↑I
e : (Quotient.mk (I ^ 2)).toSemilinearMap y = (Quotient.mk (I ^ 2)) x
⊢ x ∈ I

Proof state:
R : Type u
inst✝ : CommRing R
I : Ideal R
x : R
x✝ : (Quotient.mk (I ^ 2)) x ∈ I.cotangentIdeal
y : R
hy : y ∈ ↑I
e : (Quotient.mk (I ^ 2)).toSemilinearMap y = (Quotient.mk (I ^ 2)) x
⊢ x ∈ I

Tactic:
simpa using sub_mem hy (Ideal.pow_le_self two_ne_zero
  ((Ideal.Quotient.mk_eq_mk_iff_sub_mem _ _).mp e))

Result:
no goals