harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Computability/PostTuringMachine.lean
theorem stmts_supportsStmt {M : Λ → Stmt Γ Λ σ} {S : Finset Λ} {q : Stmt Γ Λ σ}
    (ss : Supports M S) : some q ∈ stmts M S → SupportsStmt S q

Proof state:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
inst✝ : Inhabited Λ
M : Λ → Stmt Γ Λ σ
S : Finset Λ
q : Stmt Γ Λ σ
ss : Supports M S
⊢ some q ∈ stmts M S → SupportsStmt S q

Tactic:
simp only [stmts, Finset.mem_insertNone, Finset.mem_biUnion, Option.mem_def, Option.some.injEq,
  forall_eq', exists_imp, and_imp]

Result:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
inst✝ : Inhabited Λ
M : Λ → Stmt Γ Λ σ
S : Finset Λ
q : Stmt Γ Λ σ
ss : Supports M S
⊢ ∀ x ∈ S, q ∈ stmts₁ (M x) → SupportsStmt S q

Proof state:
Γ : Type u_1
Λ : Type u_2
σ : Type u_3
inst✝ : Inhabited Λ
M : Λ → Stmt Γ Λ σ
S : Finset Λ
q : Stmt Γ Λ σ
ss : Supports M S
⊢ ∀ x ∈ S, q ∈ stmts₁ (M x) → SupportsStmt S q

Tactic:
exact fun l ls h ↦ stmts₁_supportsStmt_mono h (ss.2 _ ls)

Result:
no goals
-- Mathlib/ModelTheory/Semantics.lean
theorem LHom.onTheory_model [L'.Structure M] (φ : L →ᴸ L') [φ.IsExpansionOn M] (T : L.Theory) :
    M ⊨ φ.onTheory T ↔ M ⊨ T

Proof state:
L : Language
L' : Language
M : Type w
inst✝² : L.Structure M
inst✝¹ : L'.Structure M
φ : L →ᴸ L'
inst✝ : φ.IsExpansionOn M
T : L.Theory
⊢ M ⊨ φ.onTheory T ↔ M ⊨ T

Tactic:
simp [Theory.model_iff, LHom.onTheory]

Result:
no goals
-- Mathlib/RingTheory/Adjoin/Basic.lean
lemma adjoin_nonUnitalSubalgebra_eq_span (s : NonUnitalSubalgebra R A) :
    Subalgebra.toSubmodule (adjoin R (s : Set A)) = span R {1} ⊔ s.toSubmodule

Proof state:
R : Type uR
A : Type uA
inst✝² : CommSemiring R
inst✝¹ : CommSemiring A
inst✝ : Algebra R A
s : NonUnitalSubalgebra R A
⊢ Subalgebra.toSubmodule (adjoin R ↑s) = span R {1} ⊔ s.toSubmodule

Tactic:
rw [adjoin_eq_span, Submonoid.closure_eq_one_union, span_union, ← NonUnitalAlgebra.adjoin_eq_span,
    NonUnitalAlgebra.adjoin_eq]

Result:
no goals
-- Mathlib/NumberTheory/NumberField/CanonicalEmbedding/Basic.lean
theorem norm_smul (c : ℝ) (x : mixedSpace K) :
    mixedEmbedding.norm (c • x) = |c| ^ finrank ℚ K * (mixedEmbedding.norm x)

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
c : ℝ
x : mixedSpace K
⊢ mixedEmbedding.norm (c • x) = |c| ^ finrank ℚ K * mixedEmbedding.norm x

Tactic:
simp_rw [mixedEmbedding.norm_apply, normAtPlace_smul, mul_pow, prod_mul_distrib,
  prod_pow_eq_pow_sum, sum_mult_eq]

Result:
no goals
-- Mathlib/LinearAlgebra/AffineSpace/AffineSubspace/Defs.lean
theorem direction_inf_of_mem {s₁ s₂ : AffineSubspace k P} {p : P} (h₁ : p ∈ s₁) (h₂ : p ∈ s₂) :
    (s₁ ⊓ s₂).direction = s₁.direction ⊓ s₂.direction

Proof state:
case h
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
s₁ s₂ : AffineSubspace k P
p : P
h₁ : p ∈ s₁
h₂ : p ∈ s₂
v : V
⊢ v ∈ (s₁ ⊓ s₂).direction ↔ v ∈ s₁.direction ⊓ s₂.direction

Tactic:
rw [Submodule.mem_inf, ← vadd_mem_iff_mem_direction v h₁, ← vadd_mem_iff_mem_direction v h₂, ←
  vadd_mem_iff_mem_direction v ((mem_inf_iff p s₁ s₂).2 ⟨h₁, h₂⟩), mem_inf_iff]

Result:
no goals

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
s₁ s₂ : AffineSubspace k P
p : P
h₁ : p ∈ s₁
h₂ : p ∈ s₂
⊢ (s₁ ⊓ s₂).direction = s₁.direction ⊓ s₂.direction

Tactic:
ext v

Result:
case h
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
s₁ s₂ : AffineSubspace k P
p : P
h₁ : p ∈ s₁
h₂ : p ∈ s₂
v : V
⊢ v ∈ (s₁ ⊓ s₂).direction ↔ v ∈ s₁.direction ⊓ s₂.direction
-- Mathlib/Order/Filter/AtTopBot/Archimedean.lean
theorem tendsto_intCast_atTop_iff [StrictOrderedRing R] [Archimedean R] {f : α → ℤ}
    {l : Filter α} : Tendsto (fun n => (f n : R)) l atTop ↔ Tendsto f l atTop

Proof state:
α : Type u_1
R : Type u_2
inst✝¹ : StrictOrderedRing R
inst✝ : Archimedean R
f : α → ℤ
l : Filter α
⊢ Tendsto (fun n => ↑(f n)) l atTop ↔ Tendsto f l atTop

Tactic:
rw [← @Int.comap_cast_atTop R, tendsto_comap_iff]

Result:
α : Type u_1
R : Type u_2
inst✝¹ : StrictOrderedRing R
inst✝ : Archimedean R
f : α → ℤ
l : Filter α
⊢ Tendsto (fun n => ↑(f n)) l atTop ↔ Tendsto (Int.cast ∘ f) l atTop

Proof state:
α : Type u_1
R : Type u_2
inst✝¹ : StrictOrderedRing R
inst✝ : Archimedean R
f : α → ℤ
l : Filter α
⊢ Tendsto (fun n => ↑(f n)) l atTop ↔ Tendsto (Int.cast ∘ f) l atTop

Tactic:
rfl

Result:
no goals
-- Mathlib/Data/List/Dedup.lean
theorem tail_dedup [Inhabited α] (l : List α) :
    l.dedup.tail = if l.headI ∈ l.tail then l.tail.dedup.tail else l.tail.dedup :=
  match l with
  | [] => rfl
  | a :: l => by by_cases ha : a ∈ l <;> simp [ha, List.dedup_cons_of_mem]

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Inhabited α
l✝ : List α
a : α
l : List α
⊢ (a :: l).dedup.tail = if (a :: l).headI ∈ (a :: l).tail then (a :: l).tail.dedup.tail else (a :: l).tail.dedup

Tactic:
by_cases ha : a ∈ l <;> simp [ha, List.dedup_cons_of_mem]

Result:
no goals
-- Mathlib/FieldTheory/Minpoly/IsIntegrallyClosed.lean
theorem _root_.PowerBasis.ofGenMemAdjoin'_gen (B : PowerBasis R S) (hint : IsIntegral R x)
    (hx : B.gen ∈ adjoin R ({x} : Set S)) :
    (B.ofGenMemAdjoin' hint hx).gen = x

Proof state:
R : Type u_1
S : Type u_2
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : IsDomain R
inst✝³ : Algebra R S
inst✝² : IsDomain S
inst✝¹ : NoZeroSMulDivisors R S
inst✝ : IsIntegrallyClosed R
x : S
B : PowerBasis R S
hint : IsIntegral R x
hx : B.gen ∈ adjoin R {x}
⊢ (B.ofGenMemAdjoin' hint hx).gen = x

Tactic:
simp [PowerBasis.ofGenMemAdjoin']

Result:
no goals
-- Mathlib/Analysis/Normed/Group/Pointwise.lean
theorem IsCompact.mul_closedBall (hs : IsCompact s) (hδ : 0 ≤ δ) (x : E) :
    s * closedBall x δ = x • cthickening δ s

Proof state:
E : Type u_1
inst✝ : SeminormedCommGroup E
δ : ℝ
s : Set E
hs : IsCompact s
hδ : 0 ≤ δ
x : E
⊢ s * closedBall x δ = x • cthickening δ s

Tactic:
rw [← smul_closedBall_one, mul_smul_comm, hs.mul_closedBall_one hδ]

Result:
no goals
-- Mathlib/Data/List/Cycle.lean
theorem next_cons_concat (y : α) (hy : x ≠ y) (hx : x ∉ l)
    (h : x ∈ y :: l ++ [x] := mem_append_right _ (mem_singleton_self x)) :
    next (y :: l ++ [x]) x h = y

Proof state:
α : Type u_1
inst✝ : DecidableEq α
l : List α
x y : α
hy : x ≠ y
hx : x ∉ l
h : optParam (x ∈ y :: l ++ [x]) ⋯
⊢ (y :: l ++ [x]).next x h = y

Tactic:
rw [next, nextOr_concat]

Result:
α : Type u_1
inst✝ : DecidableEq α
l : List α
x y : α
hy : x ≠ y
hx : x ∉ l
h : optParam (x ∈ y :: l ++ [x]) ⋯
⊢ (y :: l ++ [x]).get ⟨0, ⋯⟩ = y

case h
α : Type u_1
inst✝ : DecidableEq α
l : List α
x y : α
hy : x ≠ y
hx : x ∉ l
h : optParam (x ∈ y :: l ++ [x]) ⋯
⊢ x ∉ y :: l

Proof state:
case h
α : Type u_1
inst✝ : DecidableEq α
l : List α
x y : α
hy : x ≠ y
hx : x ∉ l
h : optParam (x ∈ y :: l ++ [x]) ⋯
⊢ x ∉ y :: l

Tactic:
simp [hy, hx]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : DecidableEq α
l : List α
x y : α
hy : x ≠ y
hx : x ∉ l
h : optParam (x ∈ y :: l ++ [x]) ⋯
⊢ (y :: l ++ [x]).get ⟨0, ⋯⟩ = y

Tactic:
rfl

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem findFinIdx?_toList (p : α → Bool) (v : Array α) :
    v.toList.findFinIdx? p = (v.findFinIdx? p).map (Fin.cast (by simp))

Proof state:
α : Type u_1
p : α → Bool
v : Array α
⊢ List.findFinIdx? p v.toList = Option.map (Fin.cast ⋯) (findFinIdx? p v)

Tactic:
rcases v with ⟨v⟩

Result:
case mk
α : Type u_1
p : α → Bool
v : List α
⊢ List.findFinIdx? p { toList := v }.toList = Option.map (Fin.cast ⋯) (findFinIdx? p { toList := v })

Proof state:
case mk
α : Type u_1
p : α → Bool
v : List α
⊢ List.findFinIdx? p { toList := v }.toList = Option.map (Fin.cast ⋯) (findFinIdx? p { toList := v })

Tactic:
simp

Result:
no goals

Proof state:
α : Type ?u.536513
p : α → Bool
v : Array α
⊢ v.size = v.toList.length

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Order/Module/Defs.lean
lemma neg_of_smul_neg_left [PosSMulReflectLT α β] (h : a • b < 0) (ha : 0 ≤ a) : b < 0 :=
  lt_of_smul_lt_smul_left (by rwa [smul_zero]) ha

Proof state:
α : Type u_1
β : Type u_2
a : α
b : β
inst✝⁵ : Zero α
inst✝⁴ : Zero β
inst✝³ : SMulZeroClass α β
inst✝² : Preorder α
inst✝¹ : Preorder β
inst✝ : PosSMulReflectLT α β
h : a • b < 0
ha : 0 ≤ a
⊢ a • b < a • 0

Tactic:
rwa [smul_zero]

Result:
no goals
-- Mathlib/Topology/Constructions.lean
theorem continuous_sigma_iff {f : Sigma σ → X} :
    Continuous f ↔ ∀ i, Continuous fun a => f ⟨i, a⟩

Proof state:
X : Type u
ι : Type u_5
σ : ι → Type u_7
inst✝¹ : (i : ι) → TopologicalSpace (σ i)
inst✝ : TopologicalSpace X
f : Sigma σ → X
⊢ Continuous f ↔ ∀ (i : ι), Continuous fun a => f ⟨i, a⟩

Tactic:
rw [continuous_iSup_dom]

Result:
X : Type u
ι : Type u_5
σ : ι → Type u_7
inst✝¹ : (i : ι) → TopologicalSpace (σ i)
inst✝ : TopologicalSpace X
f : Sigma σ → X
⊢ (∀ (i : ι), Continuous f) ↔ ∀ (i : ι), Continuous fun a => f ⟨i, a⟩

Proof state:
X : Type u
ι : Type u_5
σ : ι → Type u_7
inst✝¹ : (i : ι) → TopologicalSpace (σ i)
inst✝ : TopologicalSpace X
f : Sigma σ → X
⊢ (∀ (i : ι), Continuous f) ↔ ∀ (i : ι), Continuous fun a => f ⟨i, a⟩

Tactic:
exact forall_congr' fun _ => continuous_coinduced_dom

Result:
no goals
-- Mathlib/Data/Real/EReal.lean
lemma add_lt_of_lt_sub {a b c : EReal} (h : a < b - c) : a + c < b

Proof state:
a b c : EReal
h : b ≤ a + c
⊢ b - c ≤ a

Tactic:
exact sub_le_of_le_add h

Result:
no goals

Proof state:
a b c : EReal
h : a < b - c
⊢ a + c < b

Tactic:
contrapose! h

Result:
a b c : EReal
h : b ≤ a + c
⊢ b - c ≤ a
-- Mathlib/Order/Filter/Tendsto.lean
theorem tendsto_inf {f : α → β} {x : Filter α} {y₁ y₂ : Filter β} :
    Tendsto f x (y₁ ⊓ y₂) ↔ Tendsto f x y₁ ∧ Tendsto f x y₂

Proof state:
α : Type u_1
β : Type u_2
f : α → β
x : Filter α
y₁ y₂ : Filter β
⊢ Tendsto f x (y₁ ⊓ y₂) ↔ Tendsto f x y₁ ∧ Tendsto f x y₂

Tactic:
simp only [Tendsto, le_inf_iff]

Result:
no goals
-- Mathlib/Algebra/CharP/Lemmas.lean
lemma neg_one_pow_expChar_pow : (-1 : R) ^ p ^ n = -1

Proof state:
R : Type u_1
inst✝ : Ring R
p n : ℕ
hR : ExpChar R p
⊢ (-1) ^ p ^ n + 1 ^ p ^ n = 0

Tactic:
rw [← add_pow_expChar_pow_of_commute _ _ (Commute.one_right _), neg_add_cancel,
  zero_pow (pow_ne_zero _ <| expChar_ne_zero R p)]

Result:
no goals

Proof state:
R : Type u_1
inst✝ : Ring R
p n : ℕ
hR : ExpChar R p
⊢ (-1) ^ p ^ n = -1

Tactic:
rw [eq_neg_iff_add_eq_zero]

Result:
R : Type u_1
inst✝ : Ring R
p n : ℕ
hR : ExpChar R p
⊢ (-1) ^ p ^ n + 1 = 0

Proof state:
R : Type u_1
inst✝ : Ring R
p n : ℕ
hR : ExpChar R p
⊢ (-1) ^ p ^ n + 1 = 0

Tactic:
nth_rw 2 [← one_pow (p ^ n)]

Result:
R : Type u_1
inst✝ : Ring R
p n : ℕ
hR : ExpChar R p
⊢ (-1) ^ p ^ n + 1 ^ p ^ n = 0
-- Mathlib/Tactic/ReduceModChar.lean
lemma CharP.isNat_pow {α} [Semiring α] : ∀ {f : α → ℕ → α} {a : α} {a' b b' c n n' : ℕ},
    CharP α n → f = HPow.hPow → IsNat a a' → IsNat b b' → IsNat n n' →
    Nat.mod (Nat.pow a' b') n' = c → IsNat (f a b) c
  | _, _, a, _, b, _, _, n, _, rfl, ⟨h⟩, ⟨rfl⟩, ⟨rfl⟩, rfl => ⟨by
    rw [h, Nat.cast_id, Nat.pow_eq, ← Nat.cast_pow, CharP.natCast_eq_natCast_mod α n]
    rfl⟩

Proof state:
α : Type u_1
inst✝ : Semiring α
a✝ : α
a b n : ℕ
x✝ : CharP α ↑n
h : a✝ = ↑a
⊢ ↑(a ^ b % n) = ↑((a ^ b).mod n)

Tactic:
rfl

Result:
no goals

Proof state:
α : Type u_1
inst✝ : Semiring α
a✝ : α
a b n : ℕ
x✝ : CharP α ↑n
h : a✝ = ↑a
⊢ a✝ ^ ↑b = ↑((a.pow b).mod n)

Tactic:
rw [h, Nat.cast_id, Nat.pow_eq, ← Nat.cast_pow, CharP.natCast_eq_natCast_mod α n]

Result:
α : Type u_1
inst✝ : Semiring α
a✝ : α
a b n : ℕ
x✝ : CharP α ↑n
h : a✝ = ↑a
⊢ ↑(a ^ b % n) = ↑((a ^ b).mod n)
-- Mathlib/Topology/Algebra/UniformGroup/Defs.lean
theorem Filter.HasBasis.uniformity_of_nhds_one_inv_mul {ι} {p : ι → Prop} {U : ι → Set α}
    (h : (𝓝 (1 : α)).HasBasis p U) :
    (𝓤 α).HasBasis p fun i => { x : α × α | x.1⁻¹ * x.2 ∈ U i }

Proof state:
α : Type u_1
inst✝² : UniformSpace α
inst✝¹ : Group α
inst✝ : UniformGroup α
ι : Sort u_3
p : ι → Prop
U : ι → Set α
h : (𝓝 1).HasBasis p U
⊢ (Filter.comap (fun x => x.1⁻¹ * x.2) (𝓝 1)).HasBasis p fun i => {x | x.1⁻¹ * x.2 ∈ U i}

Tactic:
exact h.comap _

Result:
no goals

Proof state:
α : Type u_1
inst✝² : UniformSpace α
inst✝¹ : Group α
inst✝ : UniformGroup α
ι : Sort u_3
p : ι → Prop
U : ι → Set α
h : (𝓝 1).HasBasis p U
⊢ (𝓤 α).HasBasis p fun i => {x | x.1⁻¹ * x.2 ∈ U i}

Tactic:
rw [uniformity_eq_comap_inv_mul_nhds_one]

Result:
α : Type u_1
inst✝² : UniformSpace α
inst✝¹ : Group α
inst✝ : UniformGroup α
ι : Sort u_3
p : ι → Prop
U : ι → Set α
h : (𝓝 1).HasBasis p U
⊢ (Filter.comap (fun x => x.1⁻¹ * x.2) (𝓝 1)).HasBasis p fun i => {x | x.1⁻¹ * x.2 ∈ U i}
-- Mathlib/NumberTheory/Transcendental/Liouville/LiouvilleWith.lean
theorem sub_nat_iff : LiouvilleWith p (x - n) ↔ LiouvilleWith p x

Proof state:
p x : ℝ
n : ℕ
⊢ LiouvilleWith p (x - ↑n) ↔ LiouvilleWith p x

Tactic:
rw [← Rat.cast_natCast, sub_rat_iff]

Result:
no goals
-- Mathlib/MeasureTheory/Function/L2Space.lean
theorem Integrable.const_inner (c : E) (hf : Integrable f μ) :
    Integrable (fun x => ⟪c, f x⟫) μ

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_2
𝕜 : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
f : α → E
c : E
hf : Integrable f μ
⊢ Integrable (fun x => inner c (f x)) μ

Tactic:
rw [← memLp_one_iff_integrable] at hf ⊢

Result:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_2
𝕜 : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
f : α → E
c : E
hf : MemLp f 1 μ
⊢ MemLp (fun x => inner c (f x)) 1 μ

Proof state:
α : Type u_1
m : MeasurableSpace α
μ : Measure α
E : Type u_2
𝕜 : Type u_3
inst✝² : RCLike 𝕜
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
f : α → E
c : E
hf : MemLp f 1 μ
⊢ MemLp (fun x => inner c (f x)) 1 μ

Tactic:
exact hf.const_inner c

Result:
no goals
-- Mathlib/Algebra/GCDMonoid/Finset.lean
theorem gcd_mul_left {a : α} : (s.gcd fun x ↦ a * f x) = normalize a * s.gcd f

Proof state:
case refine_1
α : Type u_2
β : Type u_3
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Finset β
f : β → α
a : α
⊢ (∅.gcd fun x => a * f x) = normalize a * ∅.gcd f

Tactic:
simp

Result:
no goals

Proof state:
case refine_2
α : Type u_2
β : Type u_3
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Finset β
f : β → α
a : α
b : β
t : Finset β
a✝ : b ∉ t
h : (t.gcd fun x => a * f x) = normalize a * t.gcd f
⊢ ((insert b t).gcd fun x => a * f x) = normalize a * (insert b t).gcd f

Tactic:
rw [gcd_insert, gcd_insert, h, ← gcd_mul_left]

Result:
case refine_2
α : Type u_2
β : Type u_3
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Finset β
f : β → α
a : α
b : β
t : Finset β
a✝ : b ∉ t
h : (t.gcd fun x => a * f x) = normalize a * t.gcd f
⊢ GCDMonoid.gcd (a * f b) (normalize a * t.gcd f) = GCDMonoid.gcd (a * f b) (a * t.gcd f)

Proof state:
case refine_2
α : Type u_2
β : Type u_3
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Finset β
f : β → α
a : α
⊢ ∀ ⦃a_1 : β⦄ {s : Finset β},
    a_1 ∉ s →
      (s.gcd fun x => a * f x) = normalize a * s.gcd f →
        ((insert a_1 s).gcd fun x => a * f x) = normalize a * (insert a_1 s).gcd f

Tactic:
intro b t _ h

Result:
case refine_2
α : Type u_2
β : Type u_3
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Finset β
f : β → α
a : α
b : β
t : Finset β
a✝ : b ∉ t
h : (t.gcd fun x => a * f x) = normalize a * t.gcd f
⊢ ((insert b t).gcd fun x => a * f x) = normalize a * (insert b t).gcd f

Proof state:
case refine_2
α : Type u_2
β : Type u_3
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Finset β
f : β → α
a : α
b : β
t : Finset β
a✝ : b ∉ t
h : (t.gcd fun x => a * f x) = normalize a * t.gcd f
⊢ GCDMonoid.gcd (a * f b) (normalize a * t.gcd f) = GCDMonoid.gcd (a * f b) (a * t.gcd f)

Tactic:
apply ((normalize_associated a).mul_right _).gcd_eq_right

Result:
no goals

Proof state:
α : Type u_2
β : Type u_3
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Finset β
f : β → α
a : α
⊢ (s.gcd fun x => a * f x) = normalize a * s.gcd f

Tactic:
refine s.induction_on ?_ ?_

Result:
case refine_1
α : Type u_2
β : Type u_3
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Finset β
f : β → α
a : α
⊢ (∅.gcd fun x => a * f x) = normalize a * ∅.gcd f

case refine_2
α : Type u_2
β : Type u_3
inst✝¹ : CancelCommMonoidWithZero α
inst✝ : NormalizedGCDMonoid α
s : Finset β
f : β → α
a : α
⊢ ∀ ⦃a_1 : β⦄ {s : Finset β},
    a_1 ∉ s →
      (s.gcd fun x => a * f x) = normalize a * s.gcd f →
        ((insert a_1 s).gcd fun x => a * f x) = normalize a * (insert a_1 s).gcd f
-- Mathlib/Topology/Sober.lean
theorem quasiSober_of_open_cover (S : Set (Set α)) (hS : ∀ s : S, IsOpen (s : Set α))
    [∀ s : S, QuasiSober s] (hS' : ⋃₀ S = ⊤) : QuasiSober α :=
  TopologicalSpace.IsOpenCover.quasiSober (U := fun s : S ↦ ⟨s, hS s⟩) <| by
    simpa [TopologicalSpace.IsOpenCover, ← SetLike.coe_set_eq, sUnion_eq_iUnion] using hS'

Proof state:
α : Type u_1
inst✝¹ : TopologicalSpace α
S : Set (Set α)
hS : ∀ (s : ↑S), IsOpen ↑s
inst✝ : ∀ (s : ↑S), QuasiSober ↑↑s
hS' : ⋃₀ S = ⊤
⊢ TopologicalSpace.IsOpenCover fun s => { carrier := ↑s, is_open' := ⋯ }

Tactic:
simpa [TopologicalSpace.IsOpenCover, ← SetLike.coe_set_eq, sUnion_eq_iUnion] using hS'

Result:
no goals
-- Mathlib/Algebra/Category/Grp/Images.lean
theorem image.fac : factorThruImage f ≫ image.ι f = f

Proof state:
G H : AddCommGrp
f : G ⟶ H
⊢ factorThruImage f ≫ ι f = f

Tactic:
ext

Result:
case hf.h
G H : AddCommGrp
f : G ⟶ H
x✝ : ↑G
⊢ (Hom.hom (factorThruImage f ≫ ι f)) x✝ = (Hom.hom f) x✝

Proof state:
case hf.h
G H : AddCommGrp
f : G ⟶ H
x✝ : ↑G
⊢ (Hom.hom (factorThruImage f ≫ ι f)) x✝ = (Hom.hom f) x✝

Tactic:
rfl

Result:
no goals
-- Mathlib/Analysis/Calculus/ContDiff/Operations.lean
theorem ContDiffWithinAt.div_const {f : E → 𝕜'} {n} (hf : ContDiffWithinAt 𝕜 n f s x) (c : 𝕜') :
    ContDiffWithinAt 𝕜 n (fun x => f x / c) s x

Proof state:
𝕜 : Type u_1
inst✝⁴ : NontriviallyNormedField 𝕜
E : Type uE
inst✝³ : NormedAddCommGroup E
inst✝² : NormedSpace 𝕜 E
s : Set E
x : E
𝕜' : Type u_6
inst✝¹ : NormedField 𝕜'
inst✝ : NormedAlgebra 𝕜 𝕜'
f : E → 𝕜'
n : WithTop ℕ∞
hf : ContDiffWithinAt 𝕜 n f s x
c : 𝕜'
⊢ ContDiffWithinAt 𝕜 n (fun x => f x / c) s x

Tactic:
simpa only [div_eq_mul_inv] using hf.mul contDiffWithinAt_const

Result:
no goals
-- Mathlib/Geometry/Manifold/ChartedSpace.lean
lemma isEmpty_of_chartedSpace (H : Type*) {M : Type*} [TopologicalSpace H] [TopologicalSpace M]
    [ChartedSpace H M] [IsEmpty H] : IsEmpty M

Proof state:
case inr.intro
H : Type u_5
M : Type u_6
inst✝³ : TopologicalSpace H
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : IsEmpty H
x : M
⊢ IsEmpty M

Tactic:
exact (IsEmpty.false (chartAt H x x)).elim

Result:
no goals

Proof state:
H : Type u_5
M : Type u_6
inst✝³ : TopologicalSpace H
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : IsEmpty H
⊢ IsEmpty M

Tactic:
rcases isEmpty_or_nonempty M with hM | ⟨⟨x⟩⟩

Result:
case inl
H : Type u_5
M : Type u_6
inst✝³ : TopologicalSpace H
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : IsEmpty H
hM : IsEmpty M
⊢ IsEmpty M

case inr.intro
H : Type u_5
M : Type u_6
inst✝³ : TopologicalSpace H
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : IsEmpty H
x : M
⊢ IsEmpty M

Proof state:
case inl
H : Type u_5
M : Type u_6
inst✝³ : TopologicalSpace H
inst✝² : TopologicalSpace M
inst✝¹ : ChartedSpace H M
inst✝ : IsEmpty H
hM : IsEmpty M
⊢ IsEmpty M

Tactic:
exact hM

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Option/Monadic.lean
theorem forIn'_eq_pelim [Monad m] [LawfulMonad m]
    (o : Option α) (f : (a : α) → a ∈ o → β → m (ForInStep β)) (b : β) :
    forIn' o b f =
      o.pelim (pure b) (fun a h => ForInStep.value <$> f a h b)

Proof state:
m : Type u_1 → Type u_2
α : Type u_3
β : Type u_1
inst✝¹ : Monad m
inst✝ : LawfulMonad m
o : Option α
f : (a : α) → a ∈ o → β → m (ForInStep β)
b : β
⊢ forIn' o b f = o.pelim (pure b) fun a h => ForInStep.value <$> f a h b

Tactic:
cases o <;> simp

Result:
no goals
-- Mathlib/MeasureTheory/Measure/FiniteMeasure.lean
theorem continuous_testAgainstNN_eval (f : Ω →ᵇ ℝ≥0) :
    Continuous fun μ : FiniteMeasure Ω ↦ μ.testAgainstNN f

Proof state:
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
f : Ω →ᵇ ℝ≥0
⊢ Continuous fun φ => φ f

Tactic:
exact WeakBilin.eval_continuous _ _

Result:
no goals

Proof state:
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
f : Ω →ᵇ ℝ≥0
⊢ Continuous ((fun φ => φ f) ∘ toWeakDualBCNN)

Tactic:
refine Continuous.comp ?_ (toWeakDualBCNN_continuous (Ω := Ω))

Result:
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
f : Ω →ᵇ ℝ≥0
⊢ Continuous fun φ => φ f

Proof state:
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
f : Ω →ᵇ ℝ≥0
⊢ Continuous fun μ => μ.testAgainstNN f

Tactic:
show Continuous ((fun φ : WeakDual ℝ≥0 (Ω →ᵇ ℝ≥0) ↦ φ f) ∘ toWeakDualBCNN)

Result:
Ω : Type u_1
inst✝² : MeasurableSpace Ω
inst✝¹ : TopologicalSpace Ω
inst✝ : OpensMeasurableSpace Ω
f : Ω →ᵇ ℝ≥0
⊢ Continuous ((fun φ => φ f) ∘ toWeakDualBCNN)
-- Mathlib/LinearAlgebra/RootSystem/RootPositive.lean
lemma RootPositiveForm.form_apply_root_ne_zero (i : ι) :
    B.form (P.root i) (P.root i) ≠ 0

Proof state:
ι : Type u_1
R : Type u_2
S : Type u_3
M : Type u_4
N : Type u_5
inst✝⁸ : LinearOrderedCommRing S
inst✝⁷ : CommRing R
inst✝⁶ : Algebra S R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
P : RootPairing ι R M N
inst✝¹ : P.IsValuedIn S
B : RootPositiveForm S P
inst✝ : FaithfulSMul S R
i : ι
⊢ (B.form (P.root i)) (P.root i) ≠ 0

Tactic:
obtain ⟨s, hs, hs'⟩ := B.exists_pos_eq i

Result:
case intro.intro
ι : Type u_1
R : Type u_2
S : Type u_3
M : Type u_4
N : Type u_5
inst✝⁸ : LinearOrderedCommRing S
inst✝⁷ : CommRing R
inst✝⁶ : Algebra S R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
P : RootPairing ι R M N
inst✝¹ : P.IsValuedIn S
B : RootPositiveForm S P
inst✝ : FaithfulSMul S R
i : ι
s : S
hs : s > 0
hs' : (algebraMap S R) s = (B.form (P.root i)) (P.root i)
⊢ (B.form (P.root i)) (P.root i) ≠ 0

Proof state:
case intro.intro
ι : Type u_1
R : Type u_2
S : Type u_3
M : Type u_4
N : Type u_5
inst✝⁸ : LinearOrderedCommRing S
inst✝⁷ : CommRing R
inst✝⁶ : Algebra S R
inst✝⁵ : AddCommGroup M
inst✝⁴ : Module R M
inst✝³ : AddCommGroup N
inst✝² : Module R N
P : RootPairing ι R M N
inst✝¹ : P.IsValuedIn S
B : RootPositiveForm S P
inst✝ : FaithfulSMul S R
i : ι
s : S
hs : s > 0
hs' : (algebraMap S R) s = (B.form (P.root i)) (P.root i)
⊢ (B.form (P.root i)) (P.root i) ≠ 0

Tactic:
simpa [← hs'] using hs.ne'

Result:
no goals