harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/RingTheory/LocalRing/RingHom/Basic.lean
lemma _root_.IsLocalHom.of_surjective [CommRing R] [CommRing S] [Nontrivial S] [IsLocalRing R]
    (f : R →+* S) (hf : Function.Surjective f) :
    IsLocalHom f

Proof state:
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Nontrivial S
inst✝ : IsLocalRing R
f : R →+* S
hf : Function.Surjective ⇑f
⊢ IsLocalHom f

Tactic:
have := IsLocalRing.of_surjective' f ‹_›

Result:
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Nontrivial S
inst✝ : IsLocalRing R
f : R →+* S
hf : Function.Surjective ⇑f
this : IsLocalRing S
⊢ IsLocalHom f

Proof state:
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Nontrivial S
inst✝ : IsLocalRing R
f : R →+* S
hf : Function.Surjective ⇑f
this✝ : IsLocalRing S
this : (Ideal.comap f (maximalIdeal S)).IsMaximal
⊢ maximalIdeal R ≤ Ideal.comap f (maximalIdeal S)

Tactic:
exact ((maximal_ideal_unique R).unique (inferInstanceAs (maximalIdeal R).IsMaximal) this).le

Result:
no goals

Proof state:
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Nontrivial S
inst✝ : IsLocalRing R
f : R →+* S
hf : Function.Surjective ⇑f
this : IsLocalRing S
⊢ IsLocalHom f

Tactic:
refine ((local_hom_TFAE f).out 3 0).mp ?_

Result:
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Nontrivial S
inst✝ : IsLocalRing R
f : R →+* S
hf : Function.Surjective ⇑f
this : IsLocalRing S
⊢ maximalIdeal R ≤ Ideal.comap f (maximalIdeal S)

Proof state:
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Nontrivial S
inst✝ : IsLocalRing R
f : R →+* S
hf : Function.Surjective ⇑f
this : IsLocalRing S
⊢ maximalIdeal R ≤ Ideal.comap f (maximalIdeal S)

Tactic:
have := Ideal.comap_isMaximal_of_surjective f hf (K := maximalIdeal S)

Result:
R : Type u_1
S : Type u_2
inst✝³ : CommRing R
inst✝² : CommRing S
inst✝¹ : Nontrivial S
inst✝ : IsLocalRing R
f : R →+* S
hf : Function.Surjective ⇑f
this✝ : IsLocalRing S
this : (Ideal.comap f (maximalIdeal S)).IsMaximal
⊢ maximalIdeal R ≤ Ideal.comap f (maximalIdeal S)
-- Mathlib/RingTheory/Binomial.lean
theorem smeval_ascPochhammer_nat_cast {R} [NonAssocRing R] [Pow R ℕ] [NatPowAssoc R] (n k : ℕ) :
    smeval (ascPochhammer ℕ k) (n : R) = smeval (ascPochhammer ℕ k) n

Proof state:
R : Type u_2
inst✝² : NonAssocRing R
inst✝¹ : Pow R ℕ
inst✝ : NatPowAssoc R
n k : ℕ
⊢ (ascPochhammer ℕ k).smeval ↑n = ↑((ascPochhammer ℕ k).smeval n)

Tactic:
rw [smeval_at_natCast (ascPochhammer ℕ k) n]

Result:
no goals
-- Mathlib/RingTheory/Smooth/Kaehler.lean
lemma isScalarTower_of_section_of_ker_sqZero :
    letI := g.toRingHom.toAlgebra; IsScalarTower P S (RingHom.ker (algebraMap P S))

Proof state:
case smul_assoc
R P S : Type u
inst✝⁶ : CommRing R
inst✝⁵ : CommRing P
inst✝⁴ : CommRing S
inst✝³ : Algebra R P
inst✝² : Algebra P S
inst✝¹ : Algebra R S
inst✝ : IsScalarTower R P S
g : S →ₐ[R] P
hf' : RingHom.ker (algebraMap P S) ^ 2 = ⊥
hg : (IsScalarTower.toAlgHom R P S).comp g = AlgHom.id R S
this : Algebra S P := g.toAlgebra
⊢ ∀ (x : P) (y : S) (z : ↥(RingHom.ker (algebraMap P S))), (x • y) • z = x • y • z

Tactic:
intro p s m

Result:
case smul_assoc
R P S : Type u
inst✝⁶ : CommRing R
inst✝⁵ : CommRing P
inst✝⁴ : CommRing S
inst✝³ : Algebra R P
inst✝² : Algebra P S
inst✝¹ : Algebra R S
inst✝ : IsScalarTower R P S
g : S →ₐ[R] P
hf' : RingHom.ker (algebraMap P S) ^ 2 = ⊥
hg : (IsScalarTower.toAlgHom R P S).comp g = AlgHom.id R S
this : Algebra S P := g.toAlgebra
p : P
s : S
m : ↥(RingHom.ker (algebraMap P S))
⊢ (p • s) • m = p • s • m
-- Mathlib/Data/Nat/Prime/Int.lean
theorem prime_iff_prime_int {p : ℕ} : p.Prime ↔ _root_.Prime (p : ℤ) :=
  ⟨fun hp =>
    ⟨Int.natCast_ne_zero_iff_pos.2 hp.pos, mt Int.isUnit_iff_natAbs_eq.1 hp.ne_one, fun a b h => by
      rw [← Int.dvd_natAbs, Int.natCast_dvd_natCast, Int.natAbs_mul, hp.dvd_mul] at h
      rwa [← Int.dvd_natAbs, Int.natCast_dvd_natCast, ← Int.dvd_natAbs, Int.natCast_dvd_natCast]⟩,
    fun hp =>
    Nat.prime_iff.2
      ⟨Int.natCast_ne_zero.1 hp.1,
        (mt Nat.isUnit_iff.1) fun h => by simp [h, not_prime_one] at hp, fun a b => by
        simpa only [Int.natCast_dvd_natCast, (Int.ofNat_mul _ _).symm] using hp.2.2 a b⟩⟩

Proof state:
p : ℕ
hp : Prime p
a b : ℤ
h : p ∣ a.natAbs ∨ p ∣ b.natAbs
⊢ ↑p ∣ a ∨ ↑p ∣ b

Tactic:
rwa [← Int.dvd_natAbs, Int.natCast_dvd_natCast, ← Int.dvd_natAbs, Int.natCast_dvd_natCast]

Result:
no goals

Proof state:
p : ℕ
hp : _root_.Prime ↑p
h : p = 1
⊢ False

Tactic:
simp [h, not_prime_one] at hp

Result:
no goals

Proof state:
p : ℕ
hp : _root_.Prime ↑p
a b : ℕ
⊢ p ∣ a * b → p ∣ a ∨ p ∣ b

Tactic:
simpa only [Int.natCast_dvd_natCast, (Int.ofNat_mul _ _).symm] using hp.2.2 a b

Result:
no goals

Proof state:
p : ℕ
hp : Prime p
a b : ℤ
h : ↑p ∣ a * b
⊢ ↑p ∣ a ∨ ↑p ∣ b

Tactic:
rw [← Int.dvd_natAbs, Int.natCast_dvd_natCast, Int.natAbs_mul, hp.dvd_mul] at h

Result:
p : ℕ
hp : Prime p
a b : ℤ
h : p ∣ a.natAbs ∨ p ∣ b.natAbs
⊢ ↑p ∣ a ∨ ↑p ∣ b
-- Mathlib/Analysis/SpecialFunctions/Log/Basic.lean
theorem tendsto_pow_log_div_mul_add_atTop (a b : ℝ) (n : ℕ) (ha : a ≠ 0) :
    Tendsto (fun x => log x ^ n / (a * x + b)) atTop (𝓝 0) :=
  ((tendsto_div_pow_mul_exp_add_atTop a b n ha.symm).comp tendsto_log_atTop).congr' <| by
    filter_upwards [eventually_gt_atTop (0 : ℝ)] with x hx using by simp [exp_log hx]

Proof state:
a b : ℝ
n : ℕ
ha : a ≠ 0
⊢ (fun x => x ^ n / (a * rexp x + b)) ∘ log =ᶠ[atTop] fun x => log x ^ n / (a * x + b)

Tactic:
filter_upwards [eventually_gt_atTop (0 : ℝ)] with x hx using by simp [exp_log hx]

Result:
no goals

Proof state:
a b : ℝ
n : ℕ
ha : a ≠ 0
x : ℝ
hx : 0 < x
⊢ ((fun x => x ^ n / (a * rexp x + b)) ∘ log) x = log x ^ n / (a * x + b)

Tactic:
simp [exp_log hx]

Result:
no goals
-- Mathlib/Data/List/Basic.lean
theorem length_eraseP_add_one {l : List α} {a} (al : a ∈ l) (pa : p a) :
    (l.eraseP p).length + 1 = l.length

Proof state:
α : Type u
p : α → Bool
l : List α
a : α
al : a ∈ l
pa : p a = true
w✝ : α
l₁ l₂ : List α
left✝¹ : ∀ (b : α), b ∈ l₁ → ¬p b = true
left✝ : p w✝ = true
h₁ : l = l₁ ++ w✝ :: l₂
h₂ : eraseP p l = l₁ ++ l₂
⊢ (eraseP p l).length + 1 = l.length

Tactic:
rw [h₂, h₁, length_append, length_append]

Result:
α : Type u
p : α → Bool
l : List α
a : α
al : a ∈ l
pa : p a = true
w✝ : α
l₁ l₂ : List α
left✝¹ : ∀ (b : α), b ∈ l₁ → ¬p b = true
left✝ : p w✝ = true
h₁ : l = l₁ ++ w✝ :: l₂
h₂ : eraseP p l = l₁ ++ l₂
⊢ l₁.length + l₂.length + 1 = l₁.length + (w✝ :: l₂).length

Proof state:
α : Type u
p : α → Bool
l : List α
a : α
al : a ∈ l
pa : p a = true
⊢ (eraseP p l).length + 1 = l.length

Tactic:
let ⟨_, l₁, l₂, _, _, h₁, h₂⟩ := exists_of_eraseP al pa

Result:
α : Type u
p : α → Bool
l : List α
a : α
al : a ∈ l
pa : p a = true
w✝ : α
l₁ l₂ : List α
left✝¹ : ∀ (b : α), b ∈ l₁ → ¬p b = true
left✝ : p w✝ = true
h₁ : l = l₁ ++ w✝ :: l₂
h₂ : eraseP p l = l₁ ++ l₂
⊢ (eraseP p l).length + 1 = l.length

Proof state:
α : Type u
p : α → Bool
l : List α
a : α
al : a ∈ l
pa : p a = true
w✝ : α
l₁ l₂ : List α
left✝¹ : ∀ (b : α), b ∈ l₁ → ¬p b = true
left✝ : p w✝ = true
h₁ : l = l₁ ++ w✝ :: l₂
h₂ : eraseP p l = l₁ ++ l₂
⊢ l₁.length + l₂.length + 1 = l₁.length + (w✝ :: l₂).length

Tactic:
rfl

Result:
no goals
-- Mathlib/Algebra/Order/Quantale.lean
theorem bot_mul : ⊥ * x = ⊥

Proof state:
α : Type u_3
inst✝² : Semigroup α
inst✝¹ : CompleteLattice α
inst✝ : IsQuantale α
x : α
⊢ ⊥ * x = ⊥

Tactic:
rw [← sSup_empty, sSup_mul_distrib]

Result:
α : Type u_3
inst✝² : Semigroup α
inst✝¹ : CompleteLattice α
inst✝ : IsQuantale α
x : α
⊢ ⨆ y ∈ ∅, y * x = sSup ∅

Proof state:
α : Type u_3
inst✝² : Semigroup α
inst✝¹ : CompleteLattice α
inst✝ : IsQuantale α
x : α
⊢ ⨆ y ∈ ∅, y * x = sSup ∅

Tactic:
simp only [Set.mem_empty_iff_false, not_false_eq_true, iSup_neg, iSup_bot, sSup_empty]

Result:
no goals
-- Mathlib/Topology/Instances/ENNReal/Lemmas.lean
theorem ediam_Ioo (a b : ℝ) : EMetric.diam (Ioo a b) = ENNReal.ofReal (b - a)

Proof state:
case inl
a b : ℝ
h : b ≤ a
⊢ EMetric.diam (Ioo a b) = ENNReal.ofReal (b - a)

Tactic:
simp [h]

Result:
no goals

Proof state:
case inr
a b : ℝ
h : a < b
⊢ EMetric.diam (Ioo a b) = ENNReal.ofReal (b - a)

Tactic:
rw [Real.ediam_eq (isBounded_Ioo _ _), csSup_Ioo h, csInf_Ioo h]

Result:
no goals

Proof state:
a b : ℝ
⊢ EMetric.diam (Ioo a b) = ENNReal.ofReal (b - a)

Tactic:
rcases le_or_lt b a with (h | h)

Result:
case inl
a b : ℝ
h : b ≤ a
⊢ EMetric.diam (Ioo a b) = ENNReal.ofReal (b - a)

case inr
a b : ℝ
h : a < b
⊢ EMetric.diam (Ioo a b) = ENNReal.ofReal (b - a)
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Nat/Bitwise/Lemmas.lean
theorem decide_shiftRight_mod_two_eq_one :
    decide (x >>> i % 2 = 1) = x.testBit i

Proof state:
x i : Nat
⊢ decide (x >>> i % 2 = 1) = (x >>> i % 2 == 1)

Tactic:
exact (Bool.beq_eq_decide_eq _ _).symm

Result:
no goals

Proof state:
x i : Nat
⊢ decide (x >>> i % 2 = 1) = x.testBit i

Tactic:
simp only [testBit, one_and_eq_mod_two, mod_two_bne_zero]

Result:
x i : Nat
⊢ decide (x >>> i % 2 = 1) = (x >>> i % 2 == 1)
-- Mathlib/Data/Multiset/MapFold.lean
theorem rel_map_left {s : Multiset γ} {f : γ → α} :
    ∀ {t}, Rel r (s.map f) t ↔ Rel (fun a b => r (f a) b) s t :=
  @(Multiset.induction_on s (by simp) (by simp +contextual [rel_cons_left]))

Proof state:
α : Type u_1
β : Type v
γ : Type u_2
r : α → β → Prop
s : Multiset γ
f : γ → α
⊢ ∀ (a : γ) (s : Multiset γ),
    (∀ {t : Multiset β}, Rel r (map f s) t ↔ Rel (fun a b => r (f a) b) s t) →
      ∀ {t : Multiset β}, Rel r (map f (a ::ₘ s)) t ↔ Rel (fun a b => r (f a) b) (a ::ₘ s) t

Tactic:
simp +contextual [rel_cons_left]

Result:
no goals

Proof state:
α : Type u_1
β : Type v
γ : Type u_2
r : α → β → Prop
s : Multiset γ
f : γ → α
⊢ ∀ {t : Multiset β}, Rel r (map f 0) t ↔ Rel (fun a b => r (f a) b) 0 t

Tactic:
simp

Result:
no goals
-- Mathlib/Algebra/Order/AbsoluteValue/Basic.lean
theorem le_sub (a b : R) : abv a - abv b ≤ abv (a - b) :=
  sub_le_iff_le_add.2 <| by simpa using abv.add_le (a - b) b

Proof state:
R : Type u_5
S : Type u_6
inst✝¹ : Ring R
inst✝ : OrderedRing S
abv : AbsoluteValue R S
a b : R
⊢ abv a ≤ abv (a - b) + abv b

Tactic:
simpa using abv.add_le (a - b) b

Result:
no goals
-- Mathlib/Data/Fin/Tuple/Sort.lean
theorem monotone_sort (f : Fin n → α) : Monotone (f ∘ sort f)

Proof state:
n : ℕ
α : Type u_1
inst✝ : LinearOrder α
f : Fin n → α
⊢ Monotone (f ∘ ⇑(sort f))

Tactic:
rw [self_comp_sort]

Result:
n : ℕ
α : Type u_1
inst✝ : LinearOrder α
f : Fin n → α
⊢ Monotone (graph.proj ∘ ⇑(graphEquiv₂ f))

Proof state:
n : ℕ
α : Type u_1
inst✝ : LinearOrder α
f : Fin n → α
⊢ Monotone (graph.proj ∘ ⇑(graphEquiv₂ f))

Tactic:
exact (monotone_proj f).comp (graphEquiv₂ f).monotone

Result:
no goals
-- Mathlib/Analysis/Normed/Group/Basic.lean
theorem norm_le_norm_add_norm_div (u v : E) : ‖v‖ ≤ ‖u‖ + ‖u / v‖

Proof state:
E : Type u_5
inst✝ : SeminormedGroup E
u v : E
⊢ ‖v‖ ≤ ‖u‖ + ‖u / v‖

Tactic:
rw [norm_div_rev]

Result:
E : Type u_5
inst✝ : SeminormedGroup E
u v : E
⊢ ‖v‖ ≤ ‖u‖ + ‖v / u‖

Proof state:
E : Type u_5
inst✝ : SeminormedGroup E
u v : E
⊢ ‖v‖ ≤ ‖u‖ + ‖v / u‖

Tactic:
exact norm_le_norm_add_norm_div' v u

Result:
no goals
-- Mathlib/RingTheory/PowerSeries/Derivative.lean
theorem derivative.ext {R} [CommRing R] [NoZeroSMulDivisors ℕ R] {f g} (hD : d⁄dX R f = d⁄dX R g)
    (hc : constantCoeff R f = constantCoeff R g) : f = g

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NoZeroSMulDivisors ℕ R
f g : R⟦X⟧
hD : (d⁄dX R) f = (d⁄dX R) g
hc : (constantCoeff R) f = (constantCoeff R) g
⊢ f = g

Tactic:
ext n

Result:
case h
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NoZeroSMulDivisors ℕ R
f g : R⟦X⟧
hD : (d⁄dX R) f = (d⁄dX R) g
hc : (constantCoeff R) f = (constantCoeff R) g
n : ℕ
⊢ (coeff R n) f = (coeff R n) g

Proof state:
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NoZeroSMulDivisors ℕ R
f g : R⟦X⟧
hD : (d⁄dX R) f = (d⁄dX R) g
hc : (constantCoeff R) f = (constantCoeff R) g
n : ℕ
⊢ (coeff R n) ((d⁄dX R) f) = (coeff R n) ((d⁄dX R) g)

Tactic:
rw [hD]

Result:
no goals

Proof state:
case h.zero
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NoZeroSMulDivisors ℕ R
f g : R⟦X⟧
hD : (d⁄dX R) f = (d⁄dX R) g
hc : (constantCoeff R) f = (constantCoeff R) g
⊢ (coeff R 0) f = (coeff R 0) g

Tactic:
rw [coeff_zero_eq_constantCoeff, hc]

Result:
no goals

Proof state:
case h
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NoZeroSMulDivisors ℕ R
f g : R⟦X⟧
hD : (d⁄dX R) f = (d⁄dX R) g
hc : (constantCoeff R) f = (constantCoeff R) g
n : ℕ
⊢ (coeff R n) f = (coeff R n) g

Tactic:
cases n with
| zero =>
  rw [coeff_zero_eq_constantCoeff, hc]
| succ n =>
  have equ : coeff R n (d⁄dX R f) = coeff R n (d⁄dX R g) := by rw [hD]
  rwa [coeff_derivative, coeff_derivative, ← cast_succ, mul_comm, ← nsmul_eq_mul,
    mul_comm, ← nsmul_eq_mul, smul_right_inj n.succ_ne_zero] at equ

Result:
no goals

Proof state:
case h.succ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NoZeroSMulDivisors ℕ R
f g : R⟦X⟧
hD : (d⁄dX R) f = (d⁄dX R) g
hc : (constantCoeff R) f = (constantCoeff R) g
n : ℕ
equ : (coeff R n) ((d⁄dX R) f) = (coeff R n) ((d⁄dX R) g)
⊢ (coeff R (n + 1)) f = (coeff R (n + 1)) g

Tactic:
rwa [coeff_derivative, coeff_derivative, ← cast_succ, mul_comm, ← nsmul_eq_mul,
  mul_comm, ← nsmul_eq_mul, smul_right_inj n.succ_ne_zero] at equ

Result:
no goals

Proof state:
case h.succ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NoZeroSMulDivisors ℕ R
f g : R⟦X⟧
hD : (d⁄dX R) f = (d⁄dX R) g
hc : (constantCoeff R) f = (constantCoeff R) g
n : ℕ
⊢ (coeff R (n + 1)) f = (coeff R (n + 1)) g

Tactic:
have equ : coeff R n (d⁄dX R f) = coeff R n (d⁄dX R g) := by rw [hD]

Result:
case h.succ
R : Type u_1
inst✝¹ : CommRing R
inst✝ : NoZeroSMulDivisors ℕ R
f g : R⟦X⟧
hD : (d⁄dX R) f = (d⁄dX R) g
hc : (constantCoeff R) f = (constantCoeff R) g
n : ℕ
equ : (coeff R n) ((d⁄dX R) f) = (coeff R n) ((d⁄dX R) g)
⊢ (coeff R (n + 1)) f = (coeff R (n + 1)) g
-- Mathlib/Combinatorics/SimpleGraph/Clique.lean
@[simp]
lemma cliqueFree_one : G.CliqueFree 1 ↔ IsEmpty α

Proof state:
α : Type u_1
G : SimpleGraph α
⊢ G.CliqueFree 1 ↔ IsEmpty α

Tactic:
simp [CliqueFree, isEmpty_iff]

Result:
no goals
-- Mathlib/Data/Fintype/Card.lean
theorem Finset.card_compl_add_card [DecidableEq α] [Fintype α] (s : Finset α) :
    #sᶜ + #s = Fintype.card α

Proof state:
α : Type u_1
inst✝¹ : DecidableEq α
inst✝ : Fintype α
s : Finset α
⊢ #sᶜ + #s = Fintype.card α

Tactic:
rw [Nat.add_comm, card_add_card_compl]

Result:
no goals
-- Mathlib/Data/Fin/Tuple/Finset.lean
lemma map_insertNthEquiv_filter_piFinset (P : (∀ i, α (p.succAbove i)) → Prop) [DecidablePred P] :
    {r ∈ piFinset S | P (p.removeNth r)}.map (p.insertNthEquiv α).symm.toEmbedding =
      S p ×ˢ {r ∈ piFinset (p.removeNth  S) | P r}

Proof state:
case h
n : ℕ
α : Fin (n + 1) → Type u_1
p : Fin (n + 1)
S : (i : Fin (n + 1)) → Finset (α i)
P : ((i : Fin n) → α (p.succAbove i)) → Prop
inst✝ : DecidablePred P
a✝ : α p × ((i : Fin n) → α (p.succAbove i))
⊢ a✝ ∈ map (insertNthEquiv α p).symm.toEmbedding (filter (fun r => P fun i => r (p.succAbove i)) (piFinset S)) ↔
    a✝ ∈ S p ×ˢ filter (fun r => P r) (piFinset fun i => S (p.succAbove i))

Tactic:
simp [Fin.forall_iff_succAbove p, and_assoc]

Result:
no goals

Proof state:
n : ℕ
α : Fin (n + 1) → Type u_1
p : Fin (n + 1)
S : (i : Fin (n + 1)) → Finset (α i)
P : ((i : Fin n) → α (p.succAbove i)) → Prop
inst✝ : DecidablePred P
⊢ map (insertNthEquiv α p).symm.toEmbedding (filter (fun r => P (p.removeNth r)) (piFinset S)) =
    S p ×ˢ filter (fun r => P r) (piFinset (p.removeNth S))

Tactic:
unfold removeNth

Result:
n : ℕ
α : Fin (n + 1) → Type u_1
p : Fin (n + 1)
S : (i : Fin (n + 1)) → Finset (α i)
P : ((i : Fin n) → α (p.succAbove i)) → Prop
inst✝ : DecidablePred P
⊢ map (insertNthEquiv α p).symm.toEmbedding (filter (fun r => P fun i => r (p.succAbove i)) (piFinset S)) =
    S p ×ˢ filter (fun r => P r) (piFinset fun i => S (p.succAbove i))

Proof state:
n : ℕ
α : Fin (n + 1) → Type u_1
p : Fin (n + 1)
S : (i : Fin (n + 1)) → Finset (α i)
P : ((i : Fin n) → α (p.succAbove i)) → Prop
inst✝ : DecidablePred P
⊢ map (insertNthEquiv α p).symm.toEmbedding (filter (fun r => P fun i => r (p.succAbove i)) (piFinset S)) =
    S p ×ˢ filter (fun r => P r) (piFinset fun i => S (p.succAbove i))

Tactic:
ext

Result:
case h
n : ℕ
α : Fin (n + 1) → Type u_1
p : Fin (n + 1)
S : (i : Fin (n + 1)) → Finset (α i)
P : ((i : Fin n) → α (p.succAbove i)) → Prop
inst✝ : DecidablePred P
a✝ : α p × ((i : Fin n) → α (p.succAbove i))
⊢ a✝ ∈ map (insertNthEquiv α p).symm.toEmbedding (filter (fun r => P fun i => r (p.succAbove i)) (piFinset S)) ↔
    a✝ ∈ S p ×ˢ filter (fun r => P r) (piFinset fun i => S (p.succAbove i))
-- Mathlib/Data/Finsupp/Basic.lean
theorem sigma_support : l.support = l.splitSupport.sigma fun i => (l.split i).support

Proof state:
ι : Type u_4
M : Type u_5
αs : ι → Type u_13
inst✝ : Zero M
l : (i : ι) × αs i →₀ M
⊢ l.support = l.splitSupport.sigma fun i => (l.split i).support

Tactic:
simp only [Finset.ext_iff, splitSupport, split, comapDomain, @mem_image _ _ (Classical.decEq _),
  mem_preimage, Sigma.forall, mem_sigma]

Result:
ι : Type u_4
M : Type u_5
αs : ι → Type u_13
inst✝ : Zero M
l : (i : ι) × αs i →₀ M
⊢ ∀ (a : ι) (b : αs a), ⟨a, b⟩ ∈ l.support ↔ (∃ a_1 ∈ l.support, a_1.fst = a) ∧ ⟨a, b⟩ ∈ l.support

Proof state:
ι : Type u_4
M : Type u_5
αs : ι → Type u_13
inst✝ : Zero M
l : (i : ι) × αs i →₀ M
⊢ ∀ (a : ι) (b : αs a), ⟨a, b⟩ ∈ l.support ↔ (∃ a_1 ∈ l.support, a_1.fst = a) ∧ ⟨a, b⟩ ∈ l.support

Tactic:
tauto

Result:
no goals
-- Mathlib/Analysis/InnerProductSpace/l2Space.lean
theorem hasSum_inner_mul_inner (b : HilbertBasis ι 𝕜 E) (x y : E) :
    HasSum (fun i => ⟪x, b i⟫ * ⟪b i, y⟫) ⟪x, y⟫

Proof state:
ι : Type u_1
𝕜 : Type u_2
inst✝² : RCLike 𝕜
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
b : HilbertBasis ι 𝕜 E
x y : E
⊢ HasSum (fun i => inner x (b i) * inner (b i) y) (inner x y)

Tactic:
convert (b.hasSum_repr y).mapL (innerSL 𝕜 x) using 1

Result:
case h.e'_5
ι : Type u_1
𝕜 : Type u_2
inst✝² : RCLike 𝕜
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
b : HilbertBasis ι 𝕜 E
x y : E
⊢ (fun i => inner x (b i) * inner (b i) y) = fun b_1 => ((innerSL 𝕜) x) (↑(b.repr y) b_1 • b b_1)

Proof state:
case h.e'_5.h
ι : Type u_1
𝕜 : Type u_2
inst✝² : RCLike 𝕜
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
b : HilbertBasis ι 𝕜 E
x y : E
i : ι
⊢ inner x (b i) * inner (b i) y = ((innerSL 𝕜) x) (↑(b.repr y) i • b i)

Tactic:
rw [innerSL_apply, b.repr_apply_apply, inner_smul_right, mul_comm]

Result:
no goals

Proof state:
case h.e'_5
ι : Type u_1
𝕜 : Type u_2
inst✝² : RCLike 𝕜
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
b : HilbertBasis ι 𝕜 E
x y : E
⊢ (fun i => inner x (b i) * inner (b i) y) = fun b_1 => ((innerSL 𝕜) x) (↑(b.repr y) b_1 • b b_1)

Tactic:
ext i

Result:
case h.e'_5.h
ι : Type u_1
𝕜 : Type u_2
inst✝² : RCLike 𝕜
E : Type u_3
inst✝¹ : NormedAddCommGroup E
inst✝ : InnerProductSpace 𝕜 E
b : HilbertBasis ι 𝕜 E
x y : E
i : ι
⊢ inner x (b i) * inner (b i) y = ((innerSL 𝕜) x) (↑(b.repr y) i • b i)
-- Mathlib/Combinatorics/SetFamily/AhlswedeZhang.lean
lemma truncatedInf_le : truncatedInf s a ≤ a

Proof state:
α : Type u_1
inst✝² : SemilatticeInf α
s : Finset α
a : α
inst✝¹ : DecidableRel fun x1 x2 => x1 ≤ x2
inst✝ : BoundedOrder α
⊢ (if h : a ∈ upperClosure ↑s then (filter (fun b => b ≤ a) s).inf' ⋯ id else ⊥) ≤ a

Tactic:
split_ifs with h

Result:
case pos
α : Type u_1
inst✝² : SemilatticeInf α
s : Finset α
a : α
inst✝¹ : DecidableRel fun x1 x2 => x1 ≤ x2
inst✝ : BoundedOrder α
h : a ∈ upperClosure ↑s
⊢ (filter (fun b => b ≤ a) s).inf' ⋯ id ≤ a

case neg
α : Type u_1
inst✝² : SemilatticeInf α
s : Finset α
a : α
inst✝¹ : DecidableRel fun x1 x2 => x1 ≤ x2
inst✝ : BoundedOrder α
h : a ∉ upperClosure ↑s
⊢ ⊥ ≤ a

Proof state:
α : Type u_1
inst✝² : SemilatticeInf α
s : Finset α
a : α
inst✝¹ : DecidableRel fun x1 x2 => x1 ≤ x2
inst✝ : BoundedOrder α
⊢ s.truncatedInf a ≤ a

Tactic:
unfold truncatedInf

Result:
α : Type u_1
inst✝² : SemilatticeInf α
s : Finset α
a : α
inst✝¹ : DecidableRel fun x1 x2 => x1 ≤ x2
inst✝ : BoundedOrder α
⊢ (if h : a ∈ upperClosure ↑s then (filter (fun b => b ≤ a) s).inf' ⋯ id else ⊥) ≤ a

Proof state:
case pos
α : Type u_1
inst✝² : SemilatticeInf α
s : Finset α
a : α
inst✝¹ : DecidableRel fun x1 x2 => x1 ≤ x2
inst✝ : BoundedOrder α
h : a ∈ upperClosure ↑s
⊢ (filter (fun b => b ≤ a) s).inf' ⋯ id ≤ a

Tactic:
obtain ⟨b, hb, hba⟩ := h

Result:
case pos.intro.intro
α : Type u_1
inst✝² : SemilatticeInf α
s : Finset α
a : α
inst✝¹ : DecidableRel fun x1 x2 => x1 ≤ x2
inst✝ : BoundedOrder α
b : α
hb : b ∈ ↑s
hba : b ≤ a
⊢ (filter (fun b => b ≤ a) s).inf' ⋯ id ≤ a

Proof state:
case neg
α : Type u_1
inst✝² : SemilatticeInf α
s : Finset α
a : α
inst✝¹ : DecidableRel fun x1 x2 => x1 ≤ x2
inst✝ : BoundedOrder α
h : a ∉ upperClosure ↑s
⊢ ⊥ ≤ a

Tactic:
exact bot_le

Result:
no goals

Proof state:
case pos.intro.intro
α : Type u_1
inst✝² : SemilatticeInf α
s : Finset α
a : α
inst✝¹ : DecidableRel fun x1 x2 => x1 ≤ x2
inst✝ : BoundedOrder α
b : α
hb : b ∈ ↑s
hba : b ≤ a
⊢ (filter (fun b => b ≤ a) s).inf' ⋯ id ≤ a

Tactic:
exact hba.trans' <| inf'_le id <| mem_filter.2 ⟨hb, ‹_›⟩

Result:
no goals
-- Mathlib/Algebra/Ring/Subring/Basic.lean
theorem mem_iSup_of_directed {ι} [hι : Nonempty ι] {S : ι → Subring R} (hS : Directed (· ≤ ·) S)
    {x : R} : (x ∈ ⨆ i, S i) ↔ ∃ i, x ∈ S i

Proof state:
R : Type u
inst✝ : Ring R
ι : Sort u_1
hι : Nonempty ι
S : ι → Subring R
hS : Directed (fun x1 x2 => x1 ≤ x2) S
x : R
⊢ x ∈ ⨆ i, S i ↔ ∃ i, x ∈ S i

Tactic:
refine ⟨?_, fun ⟨i, hi⟩ ↦ le_iSup S i hi⟩

Result:
R : Type u
inst✝ : Ring R
ι : Sort u_1
hι : Nonempty ι
S : ι → Subring R
hS : Directed (fun x1 x2 => x1 ≤ x2) S
x : R
⊢ x ∈ ⨆ i, S i → ∃ i, x ∈ S i

Proof state:
R : Type u
inst✝ : Ring R
ι : Sort u_1
hι : Nonempty ι
S : ι → Subring R
hS : Directed (fun x1 x2 => x1 ≤ x2) S
x : R
⊢ x ∈ ⨆ i, S i → ∃ i, x ∈ S i

Tactic:
let U : Subring R :=
  Subring.mk' (⋃ i, (S i : Set R)) (⨆ i, (S i).toSubmonoid) (⨆ i, (S i).toAddSubgroup)
    (Submonoid.coe_iSup_of_directed hS) (AddSubgroup.coe_iSup_of_directed hS)

Result:
R : Type u
inst✝ : Ring R
ι : Sort u_1
hι : Nonempty ι
S : ι → Subring R
hS : Directed (fun x1 x2 => x1 ≤ x2) S
x : R
U : Subring R := Subring.mk' (⋃ i, ↑(S i)) (⨆ i, (S i).toSubmonoid) (⨆ i, (S i).toAddSubgroup) ⋯ ⋯
⊢ x ∈ ⨆ i, S i → ∃ i, x ∈ S i

Proof state:
R : Type u
inst✝ : Ring R
ι : Sort u_1
hι : Nonempty ι
S : ι → Subring R
hS : Directed (fun x1 x2 => x1 ≤ x2) S
x : R
U : Subring R := Subring.mk' (⋃ i, ↑(S i)) (⨆ i, (S i).toSubmonoid) (⨆ i, (S i).toAddSubgroup) ⋯ ⋯
⊢ ⨆ i, S i ≤ U

Tactic:
exact iSup_le fun i x hx ↦ Set.mem_iUnion.2 ⟨i, hx⟩

Result:
no goals

Proof state:
R : Type u
inst✝ : Ring R
ι : Sort u_1
hι : Nonempty ι
S : ι → Subring R
hS : Directed (fun x1 x2 => x1 ≤ x2) S
x : R
U : Subring R := Subring.mk' (⋃ i, ↑(S i)) (⨆ i, (S i).toSubmonoid) (⨆ i, (S i).toAddSubgroup) ⋯ ⋯
this : ⨆ i, S i ≤ U
⊢ x ∈ ⨆ i, S i → ∃ i, x ∈ S i

Tactic:
simpa [U] using @this x

Result:
no goals

Proof state:
R : Type u
inst✝ : Ring R
ι : Sort u_1
hι : Nonempty ι
S : ι → Subring R
hS : Directed (fun x1 x2 => x1 ≤ x2) S
x : R
U : Subring R := Subring.mk' (⋃ i, ↑(S i)) (⨆ i, (S i).toSubmonoid) (⨆ i, (S i).toAddSubgroup) ⋯ ⋯
⊢ x ∈ ⨆ i, S i → ∃ i, x ∈ S i

Tactic:
suffices ⨆ i, S i ≤ U by simpa [U] using @this x

Result:
R : Type u
inst✝ : Ring R
ι : Sort u_1
hι : Nonempty ι
S : ι → Subring R
hS : Directed (fun x1 x2 => x1 ≤ x2) S
x : R
U : Subring R := Subring.mk' (⋃ i, ↑(S i)) (⨆ i, (S i).toSubmonoid) (⨆ i, (S i).toAddSubgroup) ⋯ ⋯
⊢ ⨆ i, S i ≤ U