harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/.lake/packages/batteries/Batteries/Data/Nat/Gcd.lean
theorem Coprime.dvd_of_dvd_mul_right (H1 : Coprime k n) (H2 : k ∣ m * n) : k ∣ m

Proof state:
k n m : Nat
H1 : k.Coprime n
H2 : k ∣ m * n
t : k ∣ (m * k).gcd (m * n) := dvd_gcd (Nat.dvd_mul_left k m) H2
⊢ k ∣ m

Tactic:
rwa [gcd_mul_left, H1.gcd_eq_one, Nat.mul_one] at t

Result:
no goals

Proof state:
k n m : Nat
H1 : k.Coprime n
H2 : k ∣ m * n
⊢ k ∣ m

Tactic:
let t := dvd_gcd (Nat.dvd_mul_left k m) H2

Result:
k n m : Nat
H1 : k.Coprime n
H2 : k ∣ m * n
t : k ∣ (m * k).gcd (m * n) := dvd_gcd (Nat.dvd_mul_left k m) H2
⊢ k ∣ m
-- Mathlib/Data/Set/Image.lean
theorem preimage_subset_preimage_iff {s t : Set α} {f : β → α} (hs : s ⊆ range f) :
    f ⁻¹' s ⊆ f ⁻¹' t ↔ s ⊆ t

Proof state:
case mpr
α : Type u_1
β : Type u_2
s t : Set α
f : β → α
hs : s ⊆ range f
h : s ⊆ t
x : β
⊢ x ∈ f ⁻¹' s → x ∈ f ⁻¹' t

Tactic:
apply h

Result:
no goals

Proof state:
α : Type u_1
β : Type u_2
s t : Set α
f : β → α
hs : s ⊆ range f
⊢ f ⁻¹' s ⊆ f ⁻¹' t ↔ s ⊆ t

Tactic:
constructor

Result:
case mp
α : Type u_1
β : Type u_2
s t : Set α
f : β → α
hs : s ⊆ range f
⊢ f ⁻¹' s ⊆ f ⁻¹' t → s ⊆ t

case mpr
α : Type u_1
β : Type u_2
s t : Set α
f : β → α
hs : s ⊆ range f
⊢ s ⊆ t → f ⁻¹' s ⊆ f ⁻¹' t

Proof state:
case mp.intro
α : Type u_1
β : Type u_2
s t : Set α
f : β → α
hs : s ⊆ range f
h : f ⁻¹' s ⊆ f ⁻¹' t
y : β
hx : f y ∈ s
⊢ f y ∈ t

Tactic:
exact h hx

Result:
no goals

Proof state:
case mpr
α : Type u_1
β : Type u_2
s t : Set α
f : β → α
hs : s ⊆ range f
⊢ s ⊆ t → f ⁻¹' s ⊆ f ⁻¹' t

Tactic:
intro h x

Result:
case mpr
α : Type u_1
β : Type u_2
s t : Set α
f : β → α
hs : s ⊆ range f
h : s ⊆ t
x : β
⊢ x ∈ f ⁻¹' s → x ∈ f ⁻¹' t

Proof state:
case mp
α : Type u_1
β : Type u_2
s t : Set α
f : β → α
hs : s ⊆ range f
⊢ f ⁻¹' s ⊆ f ⁻¹' t → s ⊆ t

Tactic:
intro h x hx

Result:
case mp
α : Type u_1
β : Type u_2
s t : Set α
f : β → α
hs : s ⊆ range f
h : f ⁻¹' s ⊆ f ⁻¹' t
x : α
hx : x ∈ s
⊢ x ∈ t

Proof state:
case mp
α : Type u_1
β : Type u_2
s t : Set α
f : β → α
hs : s ⊆ range f
h : f ⁻¹' s ⊆ f ⁻¹' t
x : α
hx : x ∈ s
⊢ x ∈ t

Tactic:
rcases hs hx with ⟨y, rfl⟩

Result:
case mp.intro
α : Type u_1
β : Type u_2
s t : Set α
f : β → α
hs : s ⊆ range f
h : f ⁻¹' s ⊆ f ⁻¹' t
y : β
hx : f y ∈ s
⊢ f y ∈ t
-- Mathlib/Order/Filter/NAry.lean
theorem map₂_pure_left : map₂ m (pure a) g = g.map (m a)

Proof state:
α : Type u_1
β : Type u_3
γ : Type u_5
m : α → β → γ
g : Filter β
a : α
⊢ map₂ m (pure a) g = map (m a) g

Tactic:
rw [← map_prod_eq_map₂, pure_prod, map_map]

Result:
α : Type u_1
β : Type u_3
γ : Type u_5
m : α → β → γ
g : Filter β
a : α
⊢ map ((fun p => m p.1 p.2) ∘ Prod.mk a) g = map (m a) g

Proof state:
α : Type u_1
β : Type u_3
γ : Type u_5
m : α → β → γ
g : Filter β
a : α
⊢ map ((fun p => m p.1 p.2) ∘ Prod.mk a) g = map (m a) g

Tactic:
rfl

Result:
no goals
-- Mathlib/Data/Matrix/Basis.lean
theorem std_basis_eq_basis_mul_basis [MulZeroOneClass α] (i : m) (j : n) :
    stdBasisMatrix i j (1 : α) =
      vecMulVec (fun i' => ite (i = i') 1 0) fun j' => ite (j = j') 1 0

Proof state:
m : Type u_2
n : Type u_3
α : Type u_5
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : MulZeroOneClass α
i : m
j : n
⊢ stdBasisMatrix i j 1 = vecMulVec (fun i' => if i = i' then 1 else 0) fun j' => if j = j' then 1 else 0

Tactic:
rw [stdBasisMatrix_eq_single_vecMulVec_single]

Result:
m : Type u_2
n : Type u_3
α : Type u_5
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : MulZeroOneClass α
i : m
j : n
⊢ vecMulVec (Pi.single i 1) (Pi.single j 1) =
    vecMulVec (fun i' => if i = i' then 1 else 0) fun j' => if j = j' then 1 else 0

Proof state:
m : Type u_2
n : Type u_3
α : Type u_5
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : MulZeroOneClass α
i : m
j : n
⊢ vecMulVec (Pi.single i 1) (Pi.single j 1) =
    vecMulVec (fun i' => if i = i' then 1 else 0) fun j' => if j = j' then 1 else 0

Tactic:
congr! with i <;> simp only [Pi.single_apply, eq_comm]

Result:
no goals
-- Mathlib/Analysis/SpecialFunctions/Pow/Deriv.lean
theorem isTheta_deriv_ofReal_cpow_const_atTop {c : ℂ} (hc : c ≠ 0) :
    deriv (fun (x : ℝ) => (x : ℂ) ^ c) =Θ[atTop] fun x => x ^ (c.re - 1)

Proof state:
case h
c : ℂ
hc : c ≠ 0
x : ℝ
hx : 0 < x
⊢ ‖↑x ^ (c - 1)‖ = x ^ (c.re - 1)

Tactic:
rw [norm_cpow_eq_rpow_re_of_pos hx, sub_re, one_re]

Result:
no goals

Proof state:
c : ℂ
hc : c ≠ 0
x : ℝ
hx : x ≠ 0
⊢ deriv (fun x => ↑x ^ c) x = c * ↑x ^ (c - 1)

Tactic:
rw [deriv_ofReal_cpow_const hx hc]

Result:
no goals

Proof state:
c : ℂ
hc : c ≠ 0
⊢ (fun x => ‖↑x ^ (c - 1)‖) =ᶠ[atTop] fun x => x ^ (c.re - 1)

Tactic:
filter_upwards [eventually_gt_atTop 0] with x hx

Result:
case h
c : ℂ
hc : c ≠ 0
x : ℝ
hx : 0 < x
⊢ ‖↑x ^ (c - 1)‖ = x ^ (c.re - 1)

Proof state:
c : ℂ
hc : c ≠ 0
⊢ (deriv fun x => ↑x ^ c) =ᶠ[atTop] fun x => c * ↑x ^ (c - 1)

Tactic:
filter_upwards [eventually_ne_atTop 0] with x hx using by rw [deriv_ofReal_cpow_const hx hc]

Result:
no goals

Proof state:
c : ℂ
hc : c ≠ 0
⊢ (deriv fun x => ↑x ^ c) =Θ[atTop] fun x => x ^ (c.re - 1)

Tactic:
calc
  _ =ᶠ[atTop] fun x : ℝ ↦ c * x ^ (c - 1) := by
    filter_upwards [eventually_ne_atTop 0] with x hx using by rw [deriv_ofReal_cpow_const hx hc]
  _ =Θ[atTop] fun x : ℝ ↦ ‖(x : ℂ) ^ (c - 1)‖ :=
    (Asymptotics.IsTheta.of_norm_eventuallyEq EventuallyEq.rfl).const_mul_left hc
  _ =ᶠ[atTop] fun x ↦ x ^ (c.re - 1) := by
    filter_upwards [eventually_gt_atTop 0] with x hx
    rw [norm_cpow_eq_rpow_re_of_pos hx, sub_re, one_re]

Result:
no goals
-- Mathlib/Topology/LocallyClosed.lean
lemma IsLocallyClosed.preimage {s : Set Y} (hs : IsLocallyClosed s)
    {f : X → Y} (hf : Continuous f) :
    IsLocallyClosed (f ⁻¹' s)

Proof state:
case intro.intro.intro.intro
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : Continuous f
U Z : Set Y
hU : IsOpen U
hZ : IsClosed Z
⊢ IsLocallyClosed (f ⁻¹' (U ∩ Z))

Tactic:
exact ⟨_, _, hU.preimage hf, hZ.preimage hf, preimage_inter⟩

Result:
no goals

Proof state:
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
s : Set Y
hs : IsLocallyClosed s
f : X → Y
hf : Continuous f
⊢ IsLocallyClosed (f ⁻¹' s)

Tactic:
obtain ⟨U, Z, hU, hZ, rfl⟩ := hs

Result:
case intro.intro.intro.intro
X : Type u_1
Y : Type u_2
inst✝¹ : TopologicalSpace X
inst✝ : TopologicalSpace Y
f : X → Y
hf : Continuous f
U Z : Set Y
hU : IsOpen U
hZ : IsClosed Z
⊢ IsLocallyClosed (f ⁻¹' (U ∩ Z))
-- Mathlib/Algebra/Lie/IdealOperations.lean
theorem comap_bracket_incl {I₁ I₂ : LieIdeal R L} :
    ⁅comap I.incl I₁, comap I.incl I₂⁆ = comap I.incl ⁅I ⊓ I₁, I ⊓ I₂⁆

Proof state:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I I₁ I₂ : LieIdeal R L
⊢ ⁅comap I.incl I₁, comap I.incl I₂⁆ = comap I.incl ⁅I ⊓ I₁, I ⊓ I₂⁆

Tactic:
conv_rhs =>
  congr
  next => skip
  rw [← I.incl_idealRange]

Result:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I I₁ I₂ : LieIdeal R L
⊢ ⁅comap I.incl I₁, comap I.incl I₂⁆ = comap I.incl ⁅I.incl.idealRange ⊓ I₁, I.incl.idealRange ⊓ I₂⁆

Proof state:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I I₁ I₂ : LieIdeal R L
⊢ ⁅comap I.incl I₁, comap I.incl I₂⁆ = ⁅comap I.incl I₁, comap I.incl I₂⁆ ⊔ I.incl.ker

Tactic:
simp only [ker_incl, sup_bot_eq]

Result:
no goals

Proof state:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I I₁ I₂ : LieIdeal R L
⊢ I.incl.IsIdealMorphism

Tactic:
exact I.incl_isIdealMorphism

Result:
no goals

Proof state:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I I₁ I₂ : LieIdeal R L
⊢ ⁅comap I.incl I₁, comap I.incl I₂⁆ = comap I.incl ⁅I.incl.idealRange ⊓ I₁, I.incl.idealRange ⊓ I₂⁆

Tactic:
rw [comap_bracket_eq]

Result:
R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I I₁ I₂ : LieIdeal R L
⊢ ⁅comap I.incl I₁, comap I.incl I₂⁆ = ⁅comap I.incl I₁, comap I.incl I₂⁆ ⊔ I.incl.ker

R : Type u
L : Type v
inst✝² : CommRing R
inst✝¹ : LieRing L
inst✝ : LieAlgebra R L
I I₁ I₂ : LieIdeal R L
⊢ I.incl.IsIdealMorphism
-- Mathlib/NumberTheory/NumberField/Basic.lean
theorem ker_algebraMap_eq_bot : RingHom.ker (algebraMap (𝓞 K) (𝓞 L)) = ⊥ :=
  (RingHom.ker_eq_bot_iff_eq_zero (algebraMap (𝓞 K) (𝓞 L))).mpr <| fun x hx => by
  have h : (algebraMap K L) x = (algebraMap (𝓞 K) (𝓞 L)) x := rfl
  simp only [hx, map_zero, map_eq_zero, RingOfIntegers.coe_eq_zero_iff] at h
  exact h

Proof state:
K : Type u_4
L : Type u_5
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x : 𝓞 K
hx : (algebraMap (𝓞 K) (𝓞 L)) x = 0
h : (algebraMap K L) ↑x = ↑((algebraMap (𝓞 K) (𝓞 L)) x)
⊢ x = 0

Tactic:
simp only [hx, map_zero, map_eq_zero, RingOfIntegers.coe_eq_zero_iff] at h

Result:
K : Type u_4
L : Type u_5
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x : 𝓞 K
hx : (algebraMap (𝓞 K) (𝓞 L)) x = 0
h : x = 0
⊢ x = 0

Proof state:
K : Type u_4
L : Type u_5
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x : 𝓞 K
hx : (algebraMap (𝓞 K) (𝓞 L)) x = 0
h : x = 0
⊢ x = 0

Tactic:
exact h

Result:
no goals

Proof state:
K : Type u_4
L : Type u_5
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x : 𝓞 K
hx : (algebraMap (𝓞 K) (𝓞 L)) x = 0
⊢ x = 0

Tactic:
have h : (algebraMap K L) x = (algebraMap (𝓞 K) (𝓞 L)) x := rfl

Result:
K : Type u_4
L : Type u_5
inst✝² : Field K
inst✝¹ : Field L
inst✝ : Algebra K L
x : 𝓞 K
hx : (algebraMap (𝓞 K) (𝓞 L)) x = 0
h : (algebraMap K L) ↑x = ↑((algebraMap (𝓞 K) (𝓞 L)) x)
⊢ x = 0
-- Mathlib/RingTheory/Kaehler/JacobiZariski.lean
@[simp]
lemma δAux_X (i) :
    δAux R Q (X i) = 0

Proof state:
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type uT
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
Q : Generators S T
i : Q.vars
⊢ (δAux R Q) (X i) = 0

Tactic:
rw [X, δAux_monomial]

Result:
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type uT
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
Q : Generators S T
i : Q.vars
⊢ ((Finsupp.single i 1).prod fun x1 x2 => Q.val x1 ^ x2) ⊗ₜ[S] (D R S) 1 = 0

Proof state:
R : Type u
S : Type v
inst✝⁶ : CommRing R
inst✝⁵ : CommRing S
inst✝⁴ : Algebra R S
T : Type uT
inst✝³ : CommRing T
inst✝² : Algebra R T
inst✝¹ : Algebra S T
inst✝ : IsScalarTower R S T
Q : Generators S T
i : Q.vars
⊢ ((Finsupp.single i 1).prod fun x1 x2 => Q.val x1 ^ x2) ⊗ₜ[S] (D R S) 1 = 0

Tactic:
simp only [Derivation.map_one_eq_zero, tmul_zero]

Result:
no goals
-- Mathlib/NumberTheory/LegendreSymbol/AddCharacter.lean
theorem sum_eq_zero_of_ne_one [IsDomain R'] {ψ : AddChar R R'} (hψ : ψ ≠ 1) : ∑ a, ψ a = 0

Proof state:
case intro
R : Type u_1
inst✝³ : AddGroup R
inst✝² : Fintype R
R' : Type u_2
inst✝¹ : CommRing R'
inst✝ : IsDomain R'
ψ : AddChar R R'
hψ : ψ ≠ 1
b : R
hb : ψ b ≠ 1
h₁ : ∑ x : R, ψ b * ψ x = ∑ a : R, ψ a
h₂ : ∑ a : R, ψ a = Finset.univ.sum ⇑ψ
⊢ ∑ a : R, ψ a = 0

Tactic:
rw [← Finset.mul_sum, h₂] at h₁

Result:
case intro
R : Type u_1
inst✝³ : AddGroup R
inst✝² : Fintype R
R' : Type u_2
inst✝¹ : CommRing R'
inst✝ : IsDomain R'
ψ : AddChar R R'
hψ : ψ ≠ 1
b : R
hb : ψ b ≠ 1
h₁ : ψ b * Finset.univ.sum ⇑ψ = Finset.univ.sum ⇑ψ
h₂ : ∑ a : R, ψ a = Finset.univ.sum ⇑ψ
⊢ ∑ a : R, ψ a = 0

Proof state:
R : Type u_1
inst✝³ : AddGroup R
inst✝² : Fintype R
R' : Type u_2
inst✝¹ : CommRing R'
inst✝ : IsDomain R'
ψ : AddChar R R'
hψ : ψ ≠ 1
⊢ ∑ a : R, ψ a = 0

Tactic:
rcases ne_one_iff.1 hψ with ⟨b, hb⟩

Result:
case intro
R : Type u_1
inst✝³ : AddGroup R
inst✝² : Fintype R
R' : Type u_2
inst✝¹ : CommRing R'
inst✝ : IsDomain R'
ψ : AddChar R R'
hψ : ψ ≠ 1
b : R
hb : ψ b ≠ 1
⊢ ∑ a : R, ψ a = 0

Proof state:
case intro
R : Type u_1
inst✝³ : AddGroup R
inst✝² : Fintype R
R' : Type u_2
inst✝¹ : CommRing R'
inst✝ : IsDomain R'
ψ : AddChar R R'
hψ : ψ ≠ 1
b : R
hb : ψ b ≠ 1
⊢ ∑ a : R, ψ a = 0

Tactic:
have h₁ : ∑ a : R, ψ (b + a) = ∑ a : R, ψ a :=
  Fintype.sum_bijective _ (AddGroup.addLeft_bijective b) _ _ fun x => rfl

Result:
case intro
R : Type u_1
inst✝³ : AddGroup R
inst✝² : Fintype R
R' : Type u_2
inst✝¹ : CommRing R'
inst✝ : IsDomain R'
ψ : AddChar R R'
hψ : ψ ≠ 1
b : R
hb : ψ b ≠ 1
h₁ : ∑ a : R, ψ (b + a) = ∑ a : R, ψ a
⊢ ∑ a : R, ψ a = 0

Proof state:
case intro
R : Type u_1
inst✝³ : AddGroup R
inst✝² : Fintype R
R' : Type u_2
inst✝¹ : CommRing R'
inst✝ : IsDomain R'
ψ : AddChar R R'
hψ : ψ ≠ 1
b : R
hb : ψ b ≠ 1
h₁ : ψ b * Finset.univ.sum ⇑ψ = Finset.univ.sum ⇑ψ
h₂ : ∑ a : R, ψ a = Finset.univ.sum ⇑ψ
⊢ ∑ a : R, ψ a = 0

Tactic:
exact eq_zero_of_mul_eq_self_left hb h₁

Result:
no goals

Proof state:
case intro
R : Type u_1
inst✝³ : AddGroup R
inst✝² : Fintype R
R' : Type u_2
inst✝¹ : CommRing R'
inst✝ : IsDomain R'
ψ : AddChar R R'
hψ : ψ ≠ 1
b : R
hb : ψ b ≠ 1
h₁ : ∑ a : R, ψ (b + a) = ∑ a : R, ψ a
⊢ ∑ a : R, ψ a = 0

Tactic:
simp_rw [map_add_eq_mul] at h₁

Result:
case intro
R : Type u_1
inst✝³ : AddGroup R
inst✝² : Fintype R
R' : Type u_2
inst✝¹ : CommRing R'
inst✝ : IsDomain R'
ψ : AddChar R R'
hψ : ψ ≠ 1
b : R
hb : ψ b ≠ 1
h₁ : ∑ x : R, ψ b * ψ x = ∑ a : R, ψ a
⊢ ∑ a : R, ψ a = 0

Proof state:
case intro
R : Type u_1
inst✝³ : AddGroup R
inst✝² : Fintype R
R' : Type u_2
inst✝¹ : CommRing R'
inst✝ : IsDomain R'
ψ : AddChar R R'
hψ : ψ ≠ 1
b : R
hb : ψ b ≠ 1
h₁ : ∑ x : R, ψ b * ψ x = ∑ a : R, ψ a
⊢ ∑ a : R, ψ a = 0

Tactic:
have h₂ : ∑ a : R, ψ a = Finset.univ.sum ↑ψ := rfl

Result:
case intro
R : Type u_1
inst✝³ : AddGroup R
inst✝² : Fintype R
R' : Type u_2
inst✝¹ : CommRing R'
inst✝ : IsDomain R'
ψ : AddChar R R'
hψ : ψ ≠ 1
b : R
hb : ψ b ≠ 1
h₁ : ∑ x : R, ψ b * ψ x = ∑ a : R, ψ a
h₂ : ∑ a : R, ψ a = Finset.univ.sum ⇑ψ
⊢ ∑ a : R, ψ a = 0
-- Mathlib/Algebra/Divisibility/Basic.lean
theorem pow_dvd_pow_of_dvd (h : a ∣ b) : ∀ n : ℕ, a ^ n ∣ b ^ n
  | 0 => by rw [pow_zero, pow_zero]
  | n + 1 => by
    rw [pow_succ, pow_succ]
    exact mul_dvd_mul (pow_dvd_pow_of_dvd h n) h

Proof state:
α : Type u_1
inst✝ : CommMonoid α
a b : α
h : a ∣ b
⊢ a ^ 0 ∣ b ^ 0

Tactic:
rw [pow_zero, pow_zero]

Result:
no goals

Proof state:
α : Type u_1
inst✝ : CommMonoid α
a b : α
h : a ∣ b
n : ℕ
⊢ a ^ n * a ∣ b ^ n * b

Tactic:
exact mul_dvd_mul (pow_dvd_pow_of_dvd h n) h

Result:
no goals

Proof state:
α : Type u_1
inst✝ : CommMonoid α
a b : α
h : a ∣ b
n : ℕ
⊢ a ^ (n + 1) ∣ b ^ (n + 1)

Tactic:
rw [pow_succ, pow_succ]

Result:
α : Type u_1
inst✝ : CommMonoid α
a b : α
h : a ∣ b
n : ℕ
⊢ a ^ n * a ∣ b ^ n * b
-- Mathlib/Algebra/Group/PNatPowAssoc.lean
theorem ppow_mul (x : M) (m n : ℕ+) : x ^ (m * n) = (x ^ m) ^ n

Proof state:
case one
M : Type u_1
inst✝² : Mul M
inst✝¹ : Pow M ℕ+
inst✝ : PNatPowAssoc M
x : M
m : ℕ+
⊢ x ^ (m * 1) = (x ^ m) ^ 1

Tactic:
rw [ppow_one, mul_one]

Result:
no goals

Proof state:
case succ
M : Type u_1
inst✝² : Mul M
inst✝¹ : Pow M ℕ+
inst✝ : PNatPowAssoc M
x : M
m k : ℕ+
hk : x ^ (m * k) = (x ^ m) ^ k
⊢ x ^ (m * (k + 1)) = (x ^ m) ^ (k + 1)

Tactic:
rw [ppow_add, ppow_one, mul_add, ppow_add, mul_one, hk]

Result:
no goals

Proof state:
M : Type u_1
inst✝² : Mul M
inst✝¹ : Pow M ℕ+
inst✝ : PNatPowAssoc M
x : M
m n : ℕ+
⊢ x ^ (m * n) = (x ^ m) ^ n

Tactic:
induction n with
| one => rw [ppow_one, mul_one]
| succ k hk => rw [ppow_add, ppow_one, mul_add, ppow_add, mul_one, hk]

Result:
no goals
-- Mathlib/Analysis/Distribution/SchwartzSpace.lean
theorem norm_le_seminorm (f : 𝓢(E, F)) (x₀ : E) : ‖f x₀‖ ≤ (SchwartzMap.seminorm 𝕜 0 0) f

Proof state:
𝕜 : Type u_1
E : Type u_4
F : Type u_5
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedField 𝕜
inst✝¹ : NormedSpace 𝕜 F
inst✝ : SMulCommClass ℝ 𝕜 F
f : 𝓢(E, F)
x₀ : E
this : ‖x₀‖ ^ 0 * ‖f x₀‖ ≤ (SchwartzMap.seminorm 𝕜 0 0) f
⊢ ‖f x₀‖ ≤ (SchwartzMap.seminorm 𝕜 0 0) f

Tactic:
rwa [pow_zero, one_mul] at this

Result:
no goals

Proof state:
𝕜 : Type u_1
E : Type u_4
F : Type u_5
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedField 𝕜
inst✝¹ : NormedSpace 𝕜 F
inst✝ : SMulCommClass ℝ 𝕜 F
f : 𝓢(E, F)
x₀ : E
⊢ ‖f x₀‖ ≤ (SchwartzMap.seminorm 𝕜 0 0) f

Tactic:
have := norm_pow_mul_le_seminorm 𝕜 f 0 x₀

Result:
𝕜 : Type u_1
E : Type u_4
F : Type u_5
inst✝⁶ : NormedAddCommGroup E
inst✝⁵ : NormedSpace ℝ E
inst✝⁴ : NormedAddCommGroup F
inst✝³ : NormedSpace ℝ F
inst✝² : NormedField 𝕜
inst✝¹ : NormedSpace 𝕜 F
inst✝ : SMulCommClass ℝ 𝕜 F
f : 𝓢(E, F)
x₀ : E
this : ‖x₀‖ ^ 0 * ‖f x₀‖ ≤ (SchwartzMap.seminorm 𝕜 0 0) f
⊢ ‖f x₀‖ ≤ (SchwartzMap.seminorm 𝕜 0 0) f
-- Mathlib/Analysis/Normed/Order/Lattice.lean
theorem norm_inf_le_add (x y : α) : ‖x ⊓ y‖ ≤ ‖x‖ + ‖y‖

Proof state:
α : Type u_1
inst✝ : NormedLatticeAddCommGroup α
x y : α
h : ‖x ⊓ y - 0 ⊓ 0‖ ≤ ‖x - 0‖ + ‖y - 0‖
⊢ ‖x ⊓ y‖ ≤ ‖x‖ + ‖y‖

Tactic:
simpa only [inf_idem, sub_zero] using h

Result:
no goals

Proof state:
α : Type u_1
inst✝ : NormedLatticeAddCommGroup α
x y : α
⊢ ‖x ⊓ y‖ ≤ ‖x‖ + ‖y‖

Tactic:
have h : ‖x ⊓ y - 0 ⊓ 0‖ ≤ ‖x - 0‖ + ‖y - 0‖ := norm_inf_sub_inf_le_add_norm x y 0 0

Result:
α : Type u_1
inst✝ : NormedLatticeAddCommGroup α
x y : α
h : ‖x ⊓ y - 0 ⊓ 0‖ ≤ ‖x - 0‖ + ‖y - 0‖
⊢ ‖x ⊓ y‖ ≤ ‖x‖ + ‖y‖
-- Mathlib/NumberTheory/Cyclotomic/Embeddings.lean
theorem nrRealPlaces_eq_zero [IsCyclotomicExtension {n} ℚ K]
    (hn : 2 < n) :
    haveI := IsCyclotomicExtension.numberField {n} ℚ K
    nrRealPlaces K = 0

Proof state:
n : ℕ+
K : Type u
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {n} ℚ K
hn : 2 < n
this : NumberField K
⊢ nrRealPlaces K = 0

Tactic:
apply (IsCyclotomicExtension.zeta_spec n ℚ K).nrRealPlaces_eq_zero_of_two_lt hn

Result:
no goals

Proof state:
n : ℕ+
K : Type u
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {n} ℚ K
hn : 2 < n
⊢ nrRealPlaces K = 0

Tactic:
have := IsCyclotomicExtension.numberField {n} ℚ K

Result:
n : ℕ+
K : Type u
inst✝² : Field K
inst✝¹ : CharZero K
inst✝ : IsCyclotomicExtension {n} ℚ K
hn : 2 < n
this : NumberField K
⊢ nrRealPlaces K = 0
-- Mathlib/Topology/Maps/Proper/Basic.lean
/-- Version of `isProperMap_iff_isClosedMap_and_compact_fibers` in terms of `cofinite` and
`cocompact`. Only works when the codomain is `T1`. -/
lemma isProperMap_iff_isClosedMap_and_tendsto_cofinite [T1Space Y] :
    IsProperMap f ↔ Continuous f ∧ IsClosedMap f ∧ Tendsto f (cocompact X) cofinite

Proof state:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : X → Y
inst✝ : T1Space Y
⊢ (Continuous f ∧ IsClosedMap f ∧ ∀ (y : Y), IsCompact (f ⁻¹' {y})) ↔
    Continuous f ∧ IsClosedMap f ∧ ∀ (x : Y), (f ⁻¹' {x})ᶜ ∈ cocompact X

Tactic:
refine and_congr_right fun f_cont ↦ and_congr_right fun _ ↦
  ⟨fun H y ↦ (H y).compl_mem_cocompact, fun H y ↦ ?_⟩

Result:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : X → Y
inst✝ : T1Space Y
f_cont : Continuous f
x✝ : IsClosedMap f
H : ∀ (x : Y), (f ⁻¹' {x})ᶜ ∈ cocompact X
y : Y
⊢ IsCompact (f ⁻¹' {y})

Proof state:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : X → Y
inst✝ : T1Space Y
f_cont : Continuous f
x✝ : IsClosedMap f
H : ∀ (x : Y), (f ⁻¹' {x})ᶜ ∈ cocompact X
y : Y
⊢ IsCompact (f ⁻¹' {y})

Tactic:
rcases mem_cocompact.mp (H y) with ⟨K, hK, hKy⟩

Result:
case intro.intro
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : X → Y
inst✝ : T1Space Y
f_cont : Continuous f
x✝ : IsClosedMap f
H : ∀ (x : Y), (f ⁻¹' {x})ᶜ ∈ cocompact X
y : Y
K : Set X
hK : IsCompact K
hKy : Kᶜ ⊆ (f ⁻¹' {y})ᶜ
⊢ IsCompact (f ⁻¹' {y})

Proof state:
case intro.intro
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : X → Y
inst✝ : T1Space Y
f_cont : Continuous f
x✝ : IsClosedMap f
H : ∀ (x : Y), (f ⁻¹' {x})ᶜ ∈ cocompact X
y : Y
K : Set X
hK : IsCompact K
hKy : Kᶜ ⊆ (f ⁻¹' {y})ᶜ
⊢ IsCompact (f ⁻¹' {y})

Tactic:
exact hK.of_isClosed_subset (isClosed_singleton.preimage f_cont)
  (compl_le_compl_iff_le.mp hKy)

Result:
no goals

Proof state:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : X → Y
inst✝ : T1Space Y
⊢ IsProperMap f ↔ Continuous f ∧ IsClosedMap f ∧ Tendsto f (cocompact X) cofinite

Tactic:
simp_rw [isProperMap_iff_isClosedMap_and_compact_fibers, Tendsto,
  le_cofinite_iff_compl_singleton_mem, mem_map, preimage_compl]

Result:
X : Type u_1
Y : Type u_2
inst✝² : TopologicalSpace X
inst✝¹ : TopologicalSpace Y
f : X → Y
inst✝ : T1Space Y
⊢ (Continuous f ∧ IsClosedMap f ∧ ∀ (y : Y), IsCompact (f ⁻¹' {y})) ↔
    Continuous f ∧ IsClosedMap f ∧ ∀ (x : Y), (f ⁻¹' {x})ᶜ ∈ cocompact X
-- Mathlib/Data/Matroid/Closure.lean
lemma closure_empty_eq_ground_iff : M.closure ∅ = M.E ↔ M = loopyOn M.E

Proof state:
α : Type u_2
M : Matroid α
h : M.closure ∅ = M.E
X : Set α
⊢ (loopyOn M.E).closure X ⊆ M.closure X

Tactic:
rw [loopyOn_closure_eq, ← h]

Result:
α : Type u_2
M : Matroid α
h : M.closure ∅ = M.E
X : Set α
⊢ M.closure ∅ ⊆ M.closure X

Proof state:
α : Type u_2
M : Matroid α
h : M.closure ∅ = M.E
X : Set α
⊢ M.closure X ⊆ (loopyOn M.E).closure X

Tactic:
simp [closure_subset_ground]

Result:
no goals

Proof state:
α : Type u_2
M : Matroid α
h : M.closure ∅ = M.E
X : Set α
⊢ M.closure ∅ ⊆ M.closure X

Tactic:
exact M.closure_mono (empty_subset _)

Result:
no goals

Proof state:
α : Type u_2
M : Matroid α
h : M = loopyOn M.E
⊢ M.closure ∅ = M.E

Tactic:
rw [h, loopyOn_closure_eq, loopyOn_ground]

Result:
no goals

Proof state:
α : Type u_2
M : Matroid α
⊢ M.closure ∅ = M.E ↔ M = loopyOn M.E

Tactic:
refine ⟨fun h ↦ ext_closure ?_, fun h ↦ by rw [h, loopyOn_closure_eq, loopyOn_ground]⟩

Result:
α : Type u_2
M : Matroid α
h : M.closure ∅ = M.E
⊢ ∀ (X : Set α), M.closure X = (loopyOn M.E).closure X

Proof state:
α : Type u_2
M : Matroid α
h : M.closure ∅ = M.E
⊢ ∀ (X : Set α), M.closure X = (loopyOn M.E).closure X

Tactic:
refine fun X ↦ subset_antisymm (by simp [closure_subset_ground]) ?_

Result:
α : Type u_2
M : Matroid α
h : M.closure ∅ = M.E
X : Set α
⊢ (loopyOn M.E).closure X ⊆ M.closure X
-- Mathlib/Analysis/Seminorm.lean
theorem closedBall_eq_biInter_ball (x r) : closedBall p x r = ⋂ ρ > r, ball p x ρ

Proof state:
𝕜 : Type u_3
E : Type u_7
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : SMul 𝕜 E
p : Seminorm 𝕜 E
x : E
r : ℝ
⊢ p.closedBall x r = ⋂ ρ, ⋂ (_ : ρ > r), p.ball x ρ

Tactic:
ext y

Result:
case h
𝕜 : Type u_3
E : Type u_7
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : SMul 𝕜 E
p : Seminorm 𝕜 E
x : E
r : ℝ
y : E
⊢ y ∈ p.closedBall x r ↔ y ∈ ⋂ ρ, ⋂ (_ : ρ > r), p.ball x ρ

Proof state:
case h
𝕜 : Type u_3
E : Type u_7
inst✝² : SeminormedRing 𝕜
inst✝¹ : AddCommGroup E
inst✝ : SMul 𝕜 E
p : Seminorm 𝕜 E
x : E
r : ℝ
y : E
⊢ y ∈ p.closedBall x r ↔ y ∈ ⋂ ρ, ⋂ (_ : ρ > r), p.ball x ρ

Tactic:
simp_rw [mem_closedBall, mem_iInter₂, mem_ball, ← forall_lt_iff_le']

Result:
no goals
-- Mathlib/Analysis/CStarAlgebra/ContinuousFunctionalCalculus/Unital.lean
lemma CFC.le_one_iff (a : A) (ha : p a

Proof state:
R : Type u_1
A : Type u_2
p : A → Prop
inst✝¹² : OrderedCommRing R
inst✝¹¹ : StarRing R
inst✝¹⁰ : MetricSpace R
inst✝⁹ : IsTopologicalRing R
inst✝⁸ : ContinuousStar R
inst✝⁷ : ∀ (α : Type ?u.847012) [inst : TopologicalSpace α], StarOrderedRing C(α, R)
inst✝⁶ : TopologicalSpace A
inst✝⁵ : Ring A
inst✝⁴ : StarRing A
inst✝³ : PartialOrder A
inst✝² : StarOrderedRing A
inst✝¹ : Algebra R A
instCFC : ContinuousFunctionalCalculus R p
inst✝ : NonnegSpectrumClass R A
a : A
ha : autoParam (p a) _auto✝
⊢ a ≤ 1 ↔ ∀ x ∈ spectrum R a, x ≤ 1

Tactic:
simpa using le_algebraMap_iff_spectrum_le (r := (1 : R)) (a := a)

Result:
no goals