harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/Normed/Lp/PiLp.lean
theorem nnnorm_equiv_symm_const' {β} [SeminormedAddCommGroup β] [Nonempty ι] (b : β) :
    ‖(WithLp.equiv p (ι → β)).symm (Function.const _ b)‖₊ =
      (Fintype.card ι : ℝ≥0) ^ (1 / p).toReal * ‖b‖₊

Proof state:
p : ℝ≥0∞
ι : Type u_2
hp : Fact (1 ≤ p)
inst✝² : Fintype ι
β : Type u_5
inst✝¹ : SeminormedAddCommGroup β
inst✝ : Nonempty ι
b : β
⊢ ‖(WithLp.equiv p (ι → β)).symm (Function.const ι b)‖₊ = ↑(Fintype.card ι) ^ (1 / p).toReal * ‖b‖₊

Tactic:
rcases em <| p = ∞ with (rfl | hp)

Result:
case inl
ι : Type u_2
inst✝² : Fintype ι
β : Type u_5
inst✝¹ : SeminormedAddCommGroup β
inst✝ : Nonempty ι
b : β
hp : Fact (1 ≤ ⊤)
⊢ ‖(WithLp.equiv ⊤ (ι → β)).symm (Function.const ι b)‖₊ = ↑(Fintype.card ι) ^ (1 / ⊤).toReal * ‖b‖₊

case inr
p : ℝ≥0∞
ι : Type u_2
hp✝ : Fact (1 ≤ p)
inst✝² : Fintype ι
β : Type u_5
inst✝¹ : SeminormedAddCommGroup β
inst✝ : Nonempty ι
b : β
hp : ¬p = ⊤
⊢ ‖(WithLp.equiv p (ι → β)).symm (Function.const ι b)‖₊ = ↑(Fintype.card ι) ^ (1 / p).toReal * ‖b‖₊

Proof state:
case inl
ι : Type u_2
inst✝² : Fintype ι
β : Type u_5
inst✝¹ : SeminormedAddCommGroup β
inst✝ : Nonempty ι
b : β
hp : Fact (1 ≤ ⊤)
⊢ ‖(WithLp.equiv ⊤ (ι → β)).symm (Function.const ι b)‖₊ = ↑(Fintype.card ι) ^ (1 / ⊤).toReal * ‖b‖₊

Tactic:
simp only [WithLp.equiv_symm_pi_apply, ENNReal.div_top, ENNReal.zero_toReal, NNReal.rpow_zero,
  one_mul, nnnorm_eq_ciSup, Function.const_apply, ciSup_const]

Result:
no goals

Proof state:
case inr
p : ℝ≥0∞
ι : Type u_2
hp✝ : Fact (1 ≤ p)
inst✝² : Fintype ι
β : Type u_5
inst✝¹ : SeminormedAddCommGroup β
inst✝ : Nonempty ι
b : β
hp : ¬p = ⊤
⊢ ‖(WithLp.equiv p (ι → β)).symm (Function.const ι b)‖₊ = ↑(Fintype.card ι) ^ (1 / p).toReal * ‖b‖₊

Tactic:
exact nnnorm_equiv_symm_const hp b

Result:
no goals
-- Mathlib/GroupTheory/Coxeter/Inversion.lean
theorem IsReduced.nodup_leftInvSeq {ω : List B} (rω : cs.IsReduced ω) : List.Nodup (lis ω)

Proof state:
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
rω : cs.IsReduced ω
⊢ (cs.leftInvSeq ω).Nodup

Tactic:
simp only [leftInvSeq_eq_reverse_rightInvSeq_reverse, nodup_reverse]

Result:
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
rω : cs.IsReduced ω
⊢ (cs.rightInvSeq ω.reverse).Nodup

Proof state:
case rω
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
rω : cs.IsReduced ω
⊢ cs.IsReduced ω.reverse

Tactic:
rwa [isReduced_reverse_iff]

Result:
no goals

Proof state:
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
rω : cs.IsReduced ω
⊢ (cs.rightInvSeq ω.reverse).Nodup

Tactic:
apply nodup_rightInvSeq

Result:
case rω
B : Type u_1
W : Type u_2
inst✝ : Group W
M : CoxeterMatrix B
cs : CoxeterSystem M W
ω : List B
rω : cs.IsReduced ω
⊢ cs.IsReduced ω.reverse
-- Mathlib/NumberTheory/LegendreSymbol/JacobiSymbol.lean
theorem trichotomy (a : ℤ) (b : ℕ) : J(a | b) = 0 ∨ J(a | b) = 1 ∨ J(a | b) = -1 :=
  ((@SignType.castHom ℤ _ _).toMonoidHom.mrange.copy {0, 1, -1} <| by
    rw [Set.pair_comm]
    exact (SignType.range_eq SignType.castHom).symm).list_prod_mem
      (by
        intro _ ha'
        rcases List.mem_pmap.mp ha' with ⟨p, hp, rfl⟩
        haveI : Fact p.Prime := ⟨prime_of_mem_primeFactorsList hp⟩
        exact quadraticChar_isQuadratic (ZMod p) a)

Proof state:
a : ℤ
b : ℕ
⊢ {0, -1, 1} = ↑(MonoidHom.mrange ↑SignType.castHom)

Tactic:
exact (SignType.range_eq SignType.castHom).symm

Result:
no goals

Proof state:
a : ℤ
b : ℕ
⊢ {0, 1, -1} = ↑(MonoidHom.mrange ↑SignType.castHom)

Tactic:
rw [Set.pair_comm]

Result:
a : ℤ
b : ℕ
⊢ {0, -1, 1} = ↑(MonoidHom.mrange ↑SignType.castHom)

Proof state:
a : ℤ
b : ℕ
x✝ : ℤ
ha' : x✝ ∈ List.pmap (fun p pp => legendreSym p a) b.primeFactorsList ⋯
⊢ x✝ ∈ (MonoidHom.mrange ↑SignType.castHom).copy {0, 1, -1} ⋯

Tactic:
rcases List.mem_pmap.mp ha' with ⟨p, hp, rfl⟩

Result:
case intro.intro
a : ℤ
b p : ℕ
hp : p ∈ b.primeFactorsList
ha' : legendreSym p a ∈ List.pmap (fun p pp => legendreSym p a) b.primeFactorsList ⋯
⊢ legendreSym p a ∈ (MonoidHom.mrange ↑SignType.castHom).copy {0, 1, -1} ⋯

Proof state:
case intro.intro
a : ℤ
b p : ℕ
hp : p ∈ b.primeFactorsList
ha' : legendreSym p a ∈ List.pmap (fun p pp => legendreSym p a) b.primeFactorsList ⋯
this : Fact (Nat.Prime p)
⊢ legendreSym p a ∈ (MonoidHom.mrange ↑SignType.castHom).copy {0, 1, -1} ⋯

Tactic:
exact quadraticChar_isQuadratic (ZMod p) a

Result:
no goals

Proof state:
a : ℤ
b : ℕ
⊢ ∀ x ∈ List.pmap (fun p pp => legendreSym p a) b.primeFactorsList ⋯,
    x ∈ (MonoidHom.mrange ↑SignType.castHom).copy {0, 1, -1} ⋯

Tactic:
intro _ ha'

Result:
a : ℤ
b : ℕ
x✝ : ℤ
ha' : x✝ ∈ List.pmap (fun p pp => legendreSym p a) b.primeFactorsList ⋯
⊢ x✝ ∈ (MonoidHom.mrange ↑SignType.castHom).copy {0, 1, -1} ⋯

Proof state:
case intro.intro
a : ℤ
b p : ℕ
hp : p ∈ b.primeFactorsList
ha' : legendreSym p a ∈ List.pmap (fun p pp => legendreSym p a) b.primeFactorsList ⋯
⊢ legendreSym p a ∈ (MonoidHom.mrange ↑SignType.castHom).copy {0, 1, -1} ⋯

Tactic:
haveI : Fact p.Prime := ⟨prime_of_mem_primeFactorsList hp⟩

Result:
case intro.intro
a : ℤ
b p : ℕ
hp : p ∈ b.primeFactorsList
ha' : legendreSym p a ∈ List.pmap (fun p pp => legendreSym p a) b.primeFactorsList ⋯
this : Fact (Nat.Prime p)
⊢ legendreSym p a ∈ (MonoidHom.mrange ↑SignType.castHom).copy {0, 1, -1} ⋯
-- Mathlib/SetTheory/Game/PGame.lean
theorem add_moveRight_inl {x : PGame} (y : PGame) (i) :
    (x + y).moveRight (toRightMovesAdd (Sum.inl i)) = x.moveRight i + y

Proof state:
x y : PGame
i : x.RightMoves
⊢ (x + y).moveRight (toRightMovesAdd (Sum.inl i)) = x.moveRight i + y

Tactic:
cases x

Result:
case mk
y : PGame
α✝ β✝ : Type u_1
a✝¹ : α✝ → PGame
a✝ : β✝ → PGame
i : (mk α✝ β✝ a✝¹ a✝).RightMoves
⊢ (mk α✝ β✝ a✝¹ a✝ + y).moveRight (toRightMovesAdd (Sum.inl i)) = (mk α✝ β✝ a✝¹ a✝).moveRight i + y

Proof state:
case mk
y : PGame
α✝ β✝ : Type u_1
a✝¹ : α✝ → PGame
a✝ : β✝ → PGame
i : (mk α✝ β✝ a✝¹ a✝).RightMoves
⊢ (mk α✝ β✝ a✝¹ a✝ + y).moveRight (toRightMovesAdd (Sum.inl i)) = (mk α✝ β✝ a✝¹ a✝).moveRight i + y

Tactic:
cases y

Result:
case mk.mk
α✝¹ β✝¹ : Type u_1
a✝³ : α✝¹ → PGame
a✝² : β✝¹ → PGame
i : (mk α✝¹ β✝¹ a✝³ a✝²).RightMoves
α✝ β✝ : Type u_1
a✝¹ : α✝ → PGame
a✝ : β✝ → PGame
⊢ (mk α✝¹ β✝¹ a✝³ a✝² + mk α✝ β✝ a✝¹ a✝).moveRight (toRightMovesAdd (Sum.inl i)) =
    (mk α✝¹ β✝¹ a✝³ a✝²).moveRight i + mk α✝ β✝ a✝¹ a✝

Proof state:
case mk.mk
α✝¹ β✝¹ : Type u_1
a✝³ : α✝¹ → PGame
a✝² : β✝¹ → PGame
i : (mk α✝¹ β✝¹ a✝³ a✝²).RightMoves
α✝ β✝ : Type u_1
a✝¹ : α✝ → PGame
a✝ : β✝ → PGame
⊢ (mk α✝¹ β✝¹ a✝³ a✝² + mk α✝ β✝ a✝¹ a✝).moveRight (toRightMovesAdd (Sum.inl i)) =
    (mk α✝¹ β✝¹ a✝³ a✝²).moveRight i + mk α✝ β✝ a✝¹ a✝

Tactic:
rfl

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/NonsingularInverse.lean
theorem det_smul_inv_vecMul_eq_cramer_transpose (A : Matrix n n α) (b : n → α) (h : IsUnit A.det) :
    A.det • b ᵥ* A⁻¹ = cramer Aᵀ b

Proof state:
n : Type u'
α : Type v
inst✝² : Fintype n
inst✝¹ : DecidableEq n
inst✝ : CommRing α
A : Matrix n n α
b : n → α
h : IsUnit A.det
⊢ A.det • b ᵥ* A⁻¹ = Aᵀ.cramer b

Tactic:
rw [← A⁻¹.transpose_transpose, vecMul_transpose, transpose_nonsing_inv, ← det_transpose,
  Aᵀ.det_smul_inv_mulVec_eq_cramer _ (isUnit_det_transpose A h)]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Lemmas.lean
theorem exists_lt_succ_right {p : Nat → Prop} :
    (∃ m, m < n + 1 ∧ p m) ↔ (∃ m, m < n ∧ p m) ∨ p n

Proof state:
n : Nat
p : Nat → Prop
⊢ (∃ m, m < n + 1 ∧ p m) ↔ (∃ m, m < n ∧ p m) ∨ p n

Tactic:
simpa using exists_lt_succ_right' (p := fun m _ => p m)

Result:
no goals
-- Mathlib/Topology/UniformSpace/UniformEmbedding.lean
theorem isUniformEmbedding_inr : IsUniformEmbedding (Sum.inr : β → α ⊕ β) :=
  isUniformEmbedding_iff'.2 ⟨Sum.inr_injective, uniformContinuous_inr, fun s hs =>
    ⟨range (Prod.map Sum.inl Sum.inl) ∪ Prod.map Sum.inr Sum.inr '' s,
      union_mem_sup range_mem_map (image_mem_map hs),
      fun x h => by simpa [Prod.map_apply'] using h⟩⟩

Proof state:
α : Type u
β : Type v
inst✝¹ : UniformSpace α
inst✝ : UniformSpace β
s : Set (β × β)
hs : s ∈ 𝓤 β
x : β × β
h : x ∈ Prod.map Sum.inr Sum.inr ⁻¹' (range (Prod.map Sum.inl Sum.inl) ∪ Prod.map Sum.inr Sum.inr '' s)
⊢ x ∈ s

Tactic:
simpa [Prod.map_apply'] using h

Result:
no goals
-- Mathlib/Analysis/Asymptotics/ExpGrowth.lean
lemma expGrowthSup_mul_le {u v : ℕ → ℝ≥0∞} (h : expGrowthSup u ≠ ⊥ ∨ expGrowthSup v ≠ ⊤)
    (h' : expGrowthSup u ≠ ⊤ ∨ expGrowthSup v ≠ ⊥) :
    expGrowthSup (u * v) ≤ expGrowthSup u + expGrowthSup v

Proof state:
u v : ℕ → ℝ≥0∞
h : expGrowthSup u ≠ ⊥ ∨ expGrowthSup v ≠ ⊤
h' : expGrowthSup u ≠ ⊤ ∨ expGrowthSup v ≠ ⊥
⊢ expGrowthSup (u * v) ≤ expGrowthSup u + expGrowthSup v

Tactic:
refine (limsup_add_le h h').trans_eq' (limsup_congr (Eventually.of_forall fun n ↦ ?_))

Result:
u v : ℕ → ℝ≥0∞
h : expGrowthSup u ≠ ⊥ ∨ expGrowthSup v ≠ ⊤
h' : expGrowthSup u ≠ ⊤ ∨ expGrowthSup v ≠ ⊥
n : ℕ
⊢ ((u * v) n).log / ↑n = ((fun n => (u n).log / ↑n) + fun n => (v n).log / ↑n) n

Proof state:
u v : ℕ → ℝ≥0∞
h : expGrowthSup u ≠ ⊥ ∨ expGrowthSup v ≠ ⊤
h' : expGrowthSup u ≠ ⊤ ∨ expGrowthSup v ≠ ⊥
n : ℕ
⊢ ((u * v) n).log / ↑n = ((fun n => (u n).log / ↑n) + fun n => (v n).log / ↑n) n

Tactic:
rw [Pi.add_apply, Pi.mul_apply, log_mul_add, add_div_of_nonneg_right n.cast_nonneg']

Result:
no goals
-- Mathlib/NumberTheory/ClassNumber/AdmissibleAbsoluteValue.lean
theorem exists_partition {ι : Type*} [Finite ι] {ε : ℝ} (hε : 0 < ε) {b : R} (hb : b ≠ 0)
    (A : ι → R) (h : abv.IsAdmissible) : ∃ t : ι → Fin (h.card ε),
      ∀ i₀ i₁, t i₀ = t i₁ → (abv (A i₁ % b - A i₀ % b) : ℝ) < abv b • ε

Proof state:
R : Type u_1
inst✝¹ : EuclideanDomain R
abv : AbsoluteValue R ℤ
ι : Type u_2
inst✝ : Finite ι
ε : ℝ
hε : 0 < ε
b : R
hb : b ≠ 0
A : ι → R
h : abv.IsAdmissible
⊢ ∃ t, ∀ (i₀ i₁ : ι), t i₀ = t i₁ → ↑(abv (A i₁ % b - A i₀ % b)) < abv b • ε

Tactic:
rcases Finite.exists_equiv_fin ι with ⟨n, ⟨e⟩⟩

Result:
case intro.intro
R : Type u_1
inst✝¹ : EuclideanDomain R
abv : AbsoluteValue R ℤ
ι : Type u_2
inst✝ : Finite ι
ε : ℝ
hε : 0 < ε
b : R
hb : b ≠ 0
A : ι → R
h : abv.IsAdmissible
n : ℕ
e : ι ≃ Fin n
⊢ ∃ t, ∀ (i₀ i₁ : ι), t i₀ = t i₁ → ↑(abv (A i₁ % b - A i₀ % b)) < abv b • ε

Proof state:
case intro.intro
R : Type u_1
inst✝¹ : EuclideanDomain R
abv : AbsoluteValue R ℤ
ι : Type u_2
inst✝ : Finite ι
ε : ℝ
hε : 0 < ε
b : R
hb : b ≠ 0
A : ι → R
h : abv.IsAdmissible
n : ℕ
e : ι ≃ Fin n
⊢ ∃ t, ∀ (i₀ i₁ : ι), t i₀ = t i₁ → ↑(abv (A i₁ % b - A i₀ % b)) < abv b • ε

Tactic:
obtain ⟨t, ht⟩ := h.exists_partition' n hε hb (A ∘ e.symm)

Result:
case intro.intro.intro
R : Type u_1
inst✝¹ : EuclideanDomain R
abv : AbsoluteValue R ℤ
ι : Type u_2
inst✝ : Finite ι
ε : ℝ
hε : 0 < ε
b : R
hb : b ≠ 0
A : ι → R
h : abv.IsAdmissible
n : ℕ
e : ι ≃ Fin n
t : Fin n → Fin (h.card ε)
ht : ∀ (i₀ i₁ : Fin n), t i₀ = t i₁ → ↑(abv ((A ∘ ⇑e.symm) i₁ % b - (A ∘ ⇑e.symm) i₀ % b)) < abv b • ε
⊢ ∃ t, ∀ (i₀ i₁ : ι), t i₀ = t i₁ → ↑(abv (A i₁ % b - A i₀ % b)) < abv b • ε

Proof state:
case intro.intro.intro
R : Type u_1
inst✝¹ : EuclideanDomain R
abv : AbsoluteValue R ℤ
ι : Type u_2
inst✝ : Finite ι
ε : ℝ
hε : 0 < ε
b : R
hb : b ≠ 0
A : ι → R
h✝ : abv.IsAdmissible
n : ℕ
e : ι ≃ Fin n
t : Fin n → Fin (h✝.card ε)
ht : ∀ (i₀ i₁ : Fin n), t i₀ = t i₁ → ↑(abv ((A ∘ ⇑e.symm) i₁ % b - (A ∘ ⇑e.symm) i₀ % b)) < abv b • ε
i₀ i₁ : ι
h : (t ∘ ⇑e) i₀ = (t ∘ ⇑e) i₁
⊢ ↑(abv (A i₁ % b - A i₀ % b)) < abv b • ε

Tactic:
convert (config := {transparency := .default})
  ht (e i₀) (e i₁) h <;> simp only [e.symm_apply_apply]

Result:
no goals

Proof state:
case intro.intro.intro
R : Type u_1
inst✝¹ : EuclideanDomain R
abv : AbsoluteValue R ℤ
ι : Type u_2
inst✝ : Finite ι
ε : ℝ
hε : 0 < ε
b : R
hb : b ≠ 0
A : ι → R
h : abv.IsAdmissible
n : ℕ
e : ι ≃ Fin n
t : Fin n → Fin (h.card ε)
ht : ∀ (i₀ i₁ : Fin n), t i₀ = t i₁ → ↑(abv ((A ∘ ⇑e.symm) i₁ % b - (A ∘ ⇑e.symm) i₀ % b)) < abv b • ε
⊢ ∃ t, ∀ (i₀ i₁ : ι), t i₀ = t i₁ → ↑(abv (A i₁ % b - A i₀ % b)) < abv b • ε

Tactic:
refine ⟨t ∘ e, fun i₀ i₁ h ↦ ?_⟩

Result:
case intro.intro.intro
R : Type u_1
inst✝¹ : EuclideanDomain R
abv : AbsoluteValue R ℤ
ι : Type u_2
inst✝ : Finite ι
ε : ℝ
hε : 0 < ε
b : R
hb : b ≠ 0
A : ι → R
h✝ : abv.IsAdmissible
n : ℕ
e : ι ≃ Fin n
t : Fin n → Fin (h✝.card ε)
ht : ∀ (i₀ i₁ : Fin n), t i₀ = t i₁ → ↑(abv ((A ∘ ⇑e.symm) i₁ % b - (A ∘ ⇑e.symm) i₀ % b)) < abv b • ε
i₀ i₁ : ι
h : (t ∘ ⇑e) i₀ = (t ∘ ⇑e) i₁
⊢ ↑(abv (A i₁ % b - A i₀ % b)) < abv b • ε
-- Mathlib/Order/WithBot.lean
lemma WithBot.toDual_lt_iff {x : WithBot α} {y : WithTop αᵒᵈ} :
    x.toDual < y ↔ WithTop.ofDual y < x

Proof state:
α : Type u_1
inst✝ : LT α
x : WithBot α
y : WithTop αᵒᵈ
⊢ WithBot.toDual x < y ↔ WithTop.ofDual y < x

Tactic:
cases x <;> cases y <;> simp [toDual_lt]

Result:
no goals
-- Mathlib/Computability/Reduce.lean
theorem manyOneReducible_toNat {p : Set α} : p ≤₀ toNat p :=
  ⟨Encodable.encode, Computable.encode, by simp [toNat, setOf]⟩

Proof state:
α : Type u
inst✝¹ : Primcodable α
inst✝ : Inhabited α
p : Set α
⊢ ∀ (a : α), p a ↔ toNat p (Encodable.encode a)

Tactic:
simp [toNat, setOf]

Result:
no goals
-- Mathlib/Order/CompleteLatticeIntervals.lean
theorem subset_sInf_of_not_bddBelow [Inhabited s] {t : Set s} (ht : ¬BddBelow t) :
    sInf t = default

Proof state:
α : Type u_2
s : Set α
inst✝² : Preorder α
inst✝¹ : InfSet α
inst✝ : Inhabited ↑s
t : Set ↑s
ht : ¬BddBelow t
⊢ sInf t = default

Tactic:
simp [sInf, ht]

Result:
no goals
-- Mathlib/Data/Bool/Set.lean
theorem range_eq {α : Type*} (f : Bool → α) : range f = {f false, f true}

Proof state:
α : Type u_1
f : Bool → α
⊢ range f = {f false, f true}

Tactic:
rw [← image_univ, univ_eq, image_pair]

Result:
no goals
-- Mathlib/RingTheory/Ideal/Prod.lean
theorem map_snd_prod (I : Ideal R) (J : Ideal S) : map (RingHom.snd R S) (prod I J) = J

Proof state:
case h
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
I : Ideal R
J : Ideal S
x : S
⊢ x ∈ map (RingHom.snd R S) (I.prod J) ↔ x ∈ J

Tactic:
rw [mem_map_iff_of_surjective (RingHom.snd R S) Prod.snd_surjective]

Result:
case h
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
I : Ideal R
J : Ideal S
x : S
⊢ (∃ x_1 ∈ I.prod J, (RingHom.snd R S) x_1 = x) ↔ x ∈ J

Proof state:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
I : Ideal R
J : Ideal S
⊢ map (RingHom.snd R S) (I.prod J) = J

Tactic:
ext x

Result:
case h
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
I : Ideal R
J : Ideal S
x : S
⊢ x ∈ map (RingHom.snd R S) (I.prod J) ↔ x ∈ J

Proof state:
case h
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
I : Ideal R
J : Ideal S
x : S
⊢ (∃ x_1 ∈ I.prod J, (RingHom.snd R S) x_1 = x) ↔ x ∈ J

Tactic:
exact
  ⟨by
    rintro ⟨x, ⟨h, rfl⟩⟩
    exact h.2, fun h => ⟨⟨0, x⟩, ⟨⟨Ideal.zero_mem _, h⟩, rfl⟩⟩⟩

Result:
no goals

Proof state:
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
I : Ideal R
J : Ideal S
x : S
⊢ (∃ x_1 ∈ I.prod J, (RingHom.snd R S) x_1 = x) → x ∈ J

Tactic:
rintro ⟨x, ⟨h, rfl⟩⟩

Result:
case intro.intro
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
I : Ideal R
J : Ideal S
x : R × S
h : x ∈ I.prod J
⊢ (RingHom.snd R S) x ∈ J

Proof state:
case intro.intro
R : Type u
S : Type v
inst✝¹ : Semiring R
inst✝ : Semiring S
I : Ideal R
J : Ideal S
x : R × S
h : x ∈ I.prod J
⊢ (RingHom.snd R S) x ∈ J

Tactic:
exact h.2

Result:
no goals
-- Mathlib/Geometry/Euclidean/Circumcenter.lean
theorem sum_circumcenterWeightsWithCircumcenter (n : ℕ) :
    ∑ i, circumcenterWeightsWithCircumcenter n i = 1

Proof state:
case h.e'_3
n : ℕ
⊢ 1 = if circumcenterIndex ∈ univ then Function.const (PointsWithCircumcenterIndex n) 1 circumcenterIndex else 0

Tactic:
simp

Result:
no goals

Proof state:
case h.e'_2.a
n : ℕ
j : PointsWithCircumcenterIndex n
a✝ : j ∈ univ
⊢ circumcenterWeightsWithCircumcenter n j =
    if j = circumcenterIndex then Function.const (PointsWithCircumcenterIndex n) 1 j else 0

Tactic:
cases j <;> simp [circumcenterWeightsWithCircumcenter]

Result:
no goals

Proof state:
n : ℕ
⊢ ∑ i : PointsWithCircumcenterIndex n, circumcenterWeightsWithCircumcenter n i = 1

Tactic:
convert sum_ite_eq' univ circumcenterIndex (Function.const _ (1 : ℝ)) with j

Result:
case h.e'_2.a
n : ℕ
j : PointsWithCircumcenterIndex n
a✝ : j ∈ univ
⊢ circumcenterWeightsWithCircumcenter n j =
    if j = circumcenterIndex then Function.const (PointsWithCircumcenterIndex n) 1 j else 0

case h.e'_3
n : ℕ
⊢ 1 = if circumcenterIndex ∈ univ then Function.const (PointsWithCircumcenterIndex n) 1 circumcenterIndex else 0
-- Mathlib/Order/Filter/Cocardinal.lean
theorem eventually_cocardinal_ne (x : α) : ∀ᶠ a in cocardinal α hreg, a ≠ x

Proof state:
α : Type u
c : Cardinal.{u}
hreg : c.IsRegular
x : α
⊢ ∀ᶠ (a : α) in cocardinal α hreg, a ≠ x

Tactic:
simpa [Set.finite_singleton x] using hreg.nat_lt 1

Result:
no goals
-- Mathlib/Analysis/Convex/Deriv.lean
theorem StrictAntiOn.strictConcaveOn_of_deriv {D : Set ℝ} (hD : Convex ℝ D) {f : ℝ → ℝ}
    (hf : ContinuousOn f D) (h_anti : StrictAntiOn (deriv f) (interior D)) :
    StrictConcaveOn ℝ D f :=
  have : StrictMonoOn (deriv (-f)) (interior D)

Proof state:
D : Set ℝ
hD : Convex ℝ D
f : ℝ → ℝ
hf : ContinuousOn f D
h_anti : StrictAntiOn (deriv f) (interior D)
⊢ StrictMonoOn (deriv (-f)) (interior D)

Tactic:
simpa only [← deriv.neg] using h_anti.neg

Result:
no goals
-- Mathlib/Algebra/Order/BigOperators/Ring/List.lean
/-- A variant of `List.prod_pos` for `CanonicallyOrderedAdd`. -/
@[simp] lemma CanonicallyOrderedAdd.list_prod_pos {α : Type*}
    [CommSemiring α] [PartialOrder α] [CanonicallyOrderedAdd α] [NoZeroDivisors α] [Nontrivial α] :
    ∀ {l : List α}, 0 < l.prod ↔ (∀ x ∈ l, (0 : α) < x)
  | [] => by simp
  | (x :: xs) => by simp_rw [List.prod_cons, List.forall_mem_cons, CanonicallyOrderedAdd.mul_pos,
    list_prod_pos]

Proof state:
α : Type u_2
inst✝⁴ : CommSemiring α
inst✝³ : PartialOrder α
inst✝² : CanonicallyOrderedAdd α
inst✝¹ : NoZeroDivisors α
inst✝ : Nontrivial α
x : α
xs : List α
⊢ 0 < (x :: xs).prod ↔ ∀ (x_1 : α), x_1 ∈ x :: xs → 0 < x_1

Tactic:
simp_rw [List.prod_cons, List.forall_mem_cons, CanonicallyOrderedAdd.mul_pos,
list_prod_pos]

Result:
no goals

Proof state:
α : Type u_2
inst✝⁴ : CommSemiring α
inst✝³ : PartialOrder α
inst✝² : CanonicallyOrderedAdd α
inst✝¹ : NoZeroDivisors α
inst✝ : Nontrivial α
⊢ 0 < [].prod ↔ ∀ (x : α), x ∈ [] → 0 < x

Tactic:
simp

Result:
no goals
-- Mathlib/Analysis/Convex/Cone/Basic.lean
theorem to_orderedSMul (S : ConvexCone 𝕜 E) (h : ∀ x y : E, x ≤ y ↔ y - x ∈ S) : OrderedSMul 𝕜 E :=
  OrderedSMul.mk'
    (by
      intro x y z xy hz
      rw [h (z • x) (z • y), ← smul_sub z y x]
      exact smul_mem S hz ((h x y).mp xy.le))

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : OrderedAddCommGroup E
inst✝ : Module 𝕜 E
S : ConvexCone 𝕜 E
h : ∀ (x y : E), x ≤ y ↔ y - x ∈ S
x y : E
z : 𝕜
xy : x < y
hz : 0 < z
⊢ z • x ≤ z • y

Tactic:
rw [h (z • x) (z • y), ← smul_sub z y x]

Result:
𝕜 : Type u_1
E : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : OrderedAddCommGroup E
inst✝ : Module 𝕜 E
S : ConvexCone 𝕜 E
h : ∀ (x y : E), x ≤ y ↔ y - x ∈ S
x y : E
z : 𝕜
xy : x < y
hz : 0 < z
⊢ z • (y - x) ∈ S

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : OrderedAddCommGroup E
inst✝ : Module 𝕜 E
S : ConvexCone 𝕜 E
h : ∀ (x y : E), x ≤ y ↔ y - x ∈ S
⊢ ∀ ⦃a b : E⦄ ⦃c : 𝕜⦄, a < b → 0 < c → c • a ≤ c • b

Tactic:
intro x y z xy hz

Result:
𝕜 : Type u_1
E : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : OrderedAddCommGroup E
inst✝ : Module 𝕜 E
S : ConvexCone 𝕜 E
h : ∀ (x y : E), x ≤ y ↔ y - x ∈ S
x y : E
z : 𝕜
xy : x < y
hz : 0 < z
⊢ z • x ≤ z • y

Proof state:
𝕜 : Type u_1
E : Type u_2
inst✝² : LinearOrderedField 𝕜
inst✝¹ : OrderedAddCommGroup E
inst✝ : Module 𝕜 E
S : ConvexCone 𝕜 E
h : ∀ (x y : E), x ≤ y ↔ y - x ∈ S
x y : E
z : 𝕜
xy : x < y
hz : 0 < z
⊢ z • (y - x) ∈ S

Tactic:
exact smul_mem S hz ((h x y).mp xy.le)

Result:
no goals
-- Mathlib/Algebra/Star/NonUnitalSubalgebra.lean
theorem coe_bot : ((⊥ : NonUnitalStarSubalgebra R A) : Set A) = {0}

Proof state:
R : Type u
A : Type v
inst✝⁷ : CommSemiring R
inst✝⁶ : StarRing R
inst✝⁵ : NonUnitalSemiring A
inst✝⁴ : StarRing A
inst✝³ : Module R A
inst✝² : IsScalarTower R A A
inst✝¹ : SMulCommClass R A A
inst✝ : StarModule R A
⊢ ↑⊥ = {0}

Tactic:
simp only [Set.ext_iff, NonUnitalStarAlgebra.mem_bot, SetLike.mem_coe, Set.mem_singleton_iff,
  forall_const]

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Finite.lean
lemma card_eq_card_finite_toFinset {s : Set α} (hs : s.Finite) : Nat.card s = hs.toFinset.card

Proof state:
α : Type u_1
s : Set α
hs : s.Finite
⊢ Nat.card ↑s = hs.toFinset.card

Tactic:
simp only [← Nat.card_eq_finsetCard, hs.mem_toFinset]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Basic.lean
theorem repeat_eq_repeatTR : @repeat = @repeatTR :=
  funext fun α => funext fun f => funext fun n => funext fun init =>
  let rec go : ∀ m n, repeatTR.loop f m (repeat f n init) = repeat f (m + n) init
    | 0,      n => by simp [repeatTR.loop]
    | succ m, n => by rw [repeatTR.loop, succ_add]; exact go m (succ n)
  (go n 0).symm

Proof state:
α : Type u_1
f : α → α
n✝ : Nat
init : α
m n : Nat
⊢ repeatTR.loop f m (f (repeat f n init)) = repeat f (m + n).succ init

Tactic:
exact go m (succ n)

Result:
no goals

Proof state:
α : Type u_1
f : α → α
n✝ : Nat
init : α
n : Nat
⊢ repeatTR.loop f 0 (repeat f n init) = repeat f (0 + n) init

Tactic:
simp [repeatTR.loop]

Result:
no goals

Proof state:
α : Type u_1
f : α → α
n✝ : Nat
init : α
m n : Nat
⊢ repeatTR.loop f m.succ (repeat f n init) = repeat f (m.succ + n) init

Tactic:
rw [repeatTR.loop, succ_add]

Result:
α : Type u_1
f : α → α
n✝ : Nat
init : α
m n : Nat
⊢ repeatTR.loop f m (f (repeat f n init)) = repeat f (m + n).succ init
-- Mathlib/Data/PNat/Factors.lean
theorem prod_factorMultiset (n : ℕ+) : (factorMultiset n).prod = n :=
  eq <| by
    dsimp [factorMultiset]
    rw [PrimeMultiset.prod_ofNatList]
    exact Nat.prod_primeFactorsList n.ne_zero

Proof state:
n : ℕ+
⊢ ↑n.factorMultiset.prod = ↑n

Tactic:
dsimp [factorMultiset]

Result:
n : ℕ+
⊢ ↑(PrimeMultiset.ofNatList (↑n).primeFactorsList ⋯).prod = ↑n

Proof state:
n : ℕ+
⊢ ↑(PrimeMultiset.ofNatList (↑n).primeFactorsList ⋯).prod = ↑n

Tactic:
rw [PrimeMultiset.prod_ofNatList]

Result:
n : ℕ+
⊢ (↑n).primeFactorsList.prod = ↑n

Proof state:
n : ℕ+
⊢ (↑n).primeFactorsList.prod = ↑n

Tactic:
exact Nat.prod_primeFactorsList n.ne_zero

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/List/Lemmas.lean
theorem map_reverse (f : α → β) (l : List α) : l.reverse.map f = (l.map f).reverse

Proof state:
α : Type u_1
β : Type u_2
f : α → β
l : List α
⊢ map f l.reverse = (map f l).reverse

Tactic:
induction l <;> simp [*]

Result:
no goals
-- Mathlib/Analysis/CStarAlgebra/GelfandDuality.lean
theorem spectrum.gelfandTransform_eq (a : A) :
    spectrum ℂ (gelfandTransform ℂ A a) = spectrum ℂ a

Proof state:
case h
A : Type u_1
inst✝² : NormedCommRing A
inst✝¹ : NormedAlgebra ℂ A
inst✝ : CompleteSpace A
a : A
z : ℂ
⊢ z ∈ spectrum ℂ ((gelfandTransform ℂ A) a) ↔ z ∈ spectrum ℂ a

Tactic:
rw [ContinuousMap.spectrum_eq_range, WeakDual.CharacterSpace.mem_spectrum_iff_exists]

Result:
case h
A : Type u_1
inst✝² : NormedCommRing A
inst✝¹ : NormedAlgebra ℂ A
inst✝ : CompleteSpace A
a : A
z : ℂ
⊢ z ∈ Set.range ⇑((gelfandTransform ℂ A) a) ↔ ∃ f, f a = z

Proof state:
A : Type u_1
inst✝² : NormedCommRing A
inst✝¹ : NormedAlgebra ℂ A
inst✝ : CompleteSpace A
a : A
⊢ spectrum ℂ ((gelfandTransform ℂ A) a) = spectrum ℂ a

Tactic:
ext z

Result:
case h
A : Type u_1
inst✝² : NormedCommRing A
inst✝¹ : NormedAlgebra ℂ A
inst✝ : CompleteSpace A
a : A
z : ℂ
⊢ z ∈ spectrum ℂ ((gelfandTransform ℂ A) a) ↔ z ∈ spectrum ℂ a

Proof state:
case h
A : Type u_1
inst✝² : NormedCommRing A
inst✝¹ : NormedAlgebra ℂ A
inst✝ : CompleteSpace A
a : A
z : ℂ
⊢ z ∈ Set.range ⇑((gelfandTransform ℂ A) a) ↔ ∃ f, f a = z

Tactic:
exact Iff.rfl

Result:
no goals