harrywsanders/mathlib_extracted huggingface dataset:
-- Mathlib/Analysis/Normed/Group/AddCircle.lean
theorem norm_div_natCast {m n : ℕ} :
    ‖(↑(↑m / ↑n * p) : AddCircle p)‖ = p * (↑(min (m % n) (n - m % n)) / n)

Proof state:
p : ℝ
hp : Fact (0 < p)
m n : ℕ
⊢ p⁻¹ * (↑m / ↑n * p) = ↑m / ↑n

Tactic:
rw [mul_comm _ p, inv_mul_cancel_left₀ hp.out.ne.symm]

Result:
no goals

Proof state:
p : ℝ
hp : Fact (0 < p)
m n : ℕ
this : p⁻¹ * (↑m / ↑n * p) = ↑m / ↑n
⊢ ‖↑(↑m / ↑n * p)‖ = p * (↑(m % n ⊓ (n - m % n)) / ↑n)

Tactic:
rw [norm_eq' p hp.out, this, abs_sub_round_div_natCast_eq]

Result:
no goals

Proof state:
p : ℝ
hp : Fact (0 < p)
m n : ℕ
⊢ ‖↑(↑m / ↑n * p)‖ = p * (↑(m % n ⊓ (n - m % n)) / ↑n)

Tactic:
have : p⁻¹ * (↑m / ↑n * p) = ↑m / ↑n := by rw [mul_comm _ p, inv_mul_cancel_left₀ hp.out.ne.symm]

Result:
p : ℝ
hp : Fact (0 < p)
m n : ℕ
this : p⁻¹ * (↑m / ↑n * p) = ↑m / ↑n
⊢ ‖↑(↑m / ↑n * p)‖ = p * (↑(m % n ⊓ (n - m % n)) / ↑n)
-- Mathlib/NumberTheory/NumberField/CanonicalEmbedding/FundamentalCone.lean
theorem torsion_unitSMul_mem_integerSet {x : mixedSpace K} {ζ : (𝓞 K)ˣ} (hζ : ζ ∈ torsion K)
    (hx : x ∈ integerSet K) : ζ • x ∈ integerSet K

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
x : mixedSpace K
ζ : (𝓞 K)ˣ
hζ : ζ ∈ torsion K
hx : x ∈ integerSet K
⊢ ζ • x ∈ integerSet K

Tactic:
obtain ⟨a, ⟨_, rfl⟩, rfl⟩ := (mem_integerSet.mp hx).2

Result:
case intro.refl
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
ζ : (𝓞 K)ˣ
hζ : ζ ∈ torsion K
a : 𝓞 K
hx : (mixedEmbedding K) ↑a ∈ integerSet K
⊢ ζ • (mixedEmbedding K) ↑a ∈ integerSet K

Proof state:
case intro.refl
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
ζ : (𝓞 K)ˣ
hζ : ζ ∈ torsion K
a : 𝓞 K
hx : (mixedEmbedding K) ↑a ∈ integerSet K
⊢ ζ • (mixedEmbedding K) ↑a ∈ integerSet K

Tactic:
refine mem_integerSet.mpr ⟨torsion_smul_mem_of_mem hx.1 hζ, ⟨ζ * a, by simp⟩⟩

Result:
no goals

Proof state:
K : Type u_1
inst✝¹ : Field K
inst✝ : NumberField K
ζ : (𝓞 K)ˣ
hζ : ζ ∈ torsion K
a : 𝓞 K
hx : (mixedEmbedding K) ↑a ∈ integerSet K
⊢ (mixedEmbedding K) ↑(↑ζ * a) = ζ • (mixedEmbedding K) ↑a

Tactic:
simp

Result:
no goals
-- Mathlib/RingTheory/PowerSeries/WellKnown.lean
theorem invOneSubPow_inv_eq_one_sub_pow :
    (invOneSubPow S d).inv = (1 - X : S⟦X⟧) ^ d

Proof state:
case succ
S : Type u_1
inst✝ : CommRing S
d✝ d : ℕ
a✝ : (invOneSubPow S d).inv = (1 - X) ^ d
⊢ (invOneSubPow S (d + 1)).inv = (1 - X) ^ (d + 1)

Tactic:
rfl

Result:
no goals

Proof state:
case zero
S : Type u_1
inst✝ : CommRing S
d : ℕ
⊢ (invOneSubPow S 0).inv = (1 - X) ^ 0

Tactic:
exact Eq.symm <| pow_zero _

Result:
no goals

Proof state:
S : Type u_1
inst✝ : CommRing S
d : ℕ
⊢ (invOneSubPow S d).inv = (1 - X) ^ d

Tactic:
induction d with
| zero => exact Eq.symm <| pow_zero _
| succ d => rfl

Result:
no goals
-- Mathlib/NumberTheory/NumberField/Embeddings.lean
theorem nrRealPlaces_eq_one_of_finrank_eq_one (h : finrank ℚ K = 1) :
    nrRealPlaces K = 1

Proof state:
K : Type u_2
inst✝¹ : Field K
inst✝ : NumberField K
h : finrank ℚ K = 1
⊢ nrRealPlaces K = 1

Tactic:
have := card_add_two_mul_card_eq_rank K

Result:
K : Type u_2
inst✝¹ : Field K
inst✝ : NumberField K
h : finrank ℚ K = 1
this : nrRealPlaces K + 2 * nrComplexPlaces K = finrank ℚ K
⊢ nrRealPlaces K = 1

Proof state:
K : Type u_2
inst✝¹ : Field K
inst✝ : NumberField K
h : finrank ℚ K = 1
this : nrRealPlaces K + 2 * nrComplexPlaces K = finrank ℚ K
⊢ nrRealPlaces K = 1

Tactic:
rwa [nrComplexPlaces_eq_zero_of_finrank_eq_one h, h, mul_zero, add_zero] at this

Result:
no goals
-- Mathlib/Data/Fin/Basic.lean
theorem add_one_le_of_lt {n : ℕ} {a b : Fin (n + 1)} (h : a < b) : a + 1 ≤ b

Proof state:
n : ℕ
a b : Fin (n + 1)
h : a < b
⊢ a + 1 ≤ b

Tactic:
cases n <;> fin_omega

Result:
no goals
-- Mathlib/Analysis/Fourier/FiniteAbelian/PontryaginDuality.lean
@[simp] lemma zmod_add : ∀ x y : ZMod n, zmod n (x + y) = zmod n x * zmod n y

Proof state:
n : ℕ
inst✝ : NeZero n
⊢ ∀ (x y : ZMod n), zmod n (x + y) = zmod n x * zmod n y

Tactic:
simp [DFunLike.ext_iff, ← Int.cast_add, zmod, add_mul, add_div, map_add_eq_mul]

Result:
no goals
-- Mathlib/Algebra/ContinuedFractions/TerminatedStable.lean
theorem conts_stable_of_terminated (n_le_m : n ≤ m) (terminatedAt_n : g.TerminatedAt n) :
    g.conts m = g.conts n

Proof state:
K : Type u_1
g : GenContFract K
n m : ℕ
inst✝ : DivisionRing K
n_le_m : n ≤ m
terminatedAt_n : g.TerminatedAt n
⊢ g.conts m = g.conts n

Tactic:
simp only [nth_cont_eq_succ_nth_contAux,
  contsAux_stable_of_terminated (Nat.pred_le_iff.mp n_le_m) terminatedAt_n]

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Array/Lemmas.lean
theorem filterMap_flatMap {β γ} (l : Array α) (g : α → Array β) (f : β → Option γ) :
    (l.flatMap g).filterMap f = l.flatMap fun a => (g a).filterMap f

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
l : Array α
g : α → Array β
f : β → Option γ
⊢ filterMap f (flatMap g l) = flatMap (fun a => filterMap f (g a)) l

Tactic:
rcases l with ⟨l⟩

Result:
case mk
α : Type u_1
β : Type u_2
γ : Type u_3
g : α → Array β
f : β → Option γ
l : List α
⊢ filterMap f (flatMap g { toList := l }) = flatMap (fun a => filterMap f (g a)) { toList := l }

Proof state:
case mk
α : Type u_1
β : Type u_2
γ : Type u_3
g : α → Array β
f : β → Option γ
l : List α
⊢ filterMap f (flatMap g { toList := l }) = flatMap (fun a => filterMap f (g a)) { toList := l }

Tactic:
simp [List.filterMap_flatMap]

Result:
no goals
-- Mathlib/Geometry/Euclidean/Angle/Oriented/Affine.lean
theorem left_ne_right_of_oangle_sign_eq_neg_one {p₁ p₂ p₃ : P} (h : (∡ p₁ p₂ p₃).sign = -1) :
    p₁ ≠ p₃ :=
  left_ne_right_of_oangle_sign_ne_zero (h.symm ▸ by decide : (∡ p₁ p₂ p₃).sign ≠ 0)

Proof state:
V : Type u_1
P : Type u_2
inst✝⁴ : NormedAddCommGroup V
inst✝³ : InnerProductSpace ℝ V
inst✝² : MetricSpace P
inst✝¹ : NormedAddTorsor V P
hd2 : Fact (finrank ℝ V = 2)
inst✝ : Oriented ℝ V (Fin 2)
p₁ p₂ p₃ : P
h : (∡ p₁ p₂ p₃).sign = -1
⊢ -1 ≠ 0

Tactic:
decide

Result:
no goals
-- Mathlib/MeasureTheory/Constructions/Cylinders.lean
theorem union_mem_measurableCylinders (hs : s ∈ measurableCylinders α)
    (ht : t ∈ measurableCylinders α) :
    s ∪ t ∈ measurableCylinders α

Proof state:
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → MeasurableSpace (α i)
s t : Set ((i : ι) → α i)
hs : s ∈ measurableCylinders α
ht : t ∈ measurableCylinders α
⊢ (sᶜ ∩ tᶜ)ᶜ ∈ measurableCylinders α

Tactic:
exact compl_mem_measurableCylinders (inter_mem_measurableCylinders
  (compl_mem_measurableCylinders hs) (compl_mem_measurableCylinders ht))

Result:
no goals

Proof state:
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → MeasurableSpace (α i)
s t : Set ((i : ι) → α i)
hs : s ∈ measurableCylinders α
ht : t ∈ measurableCylinders α
⊢ s ∪ t ∈ measurableCylinders α

Tactic:
rw [union_eq_compl_compl_inter_compl]

Result:
ι : Type u_1
α : ι → Type u_2
inst✝ : (i : ι) → MeasurableSpace (α i)
s t : Set ((i : ι) → α i)
hs : s ∈ measurableCylinders α
ht : t ∈ measurableCylinders α
⊢ (sᶜ ∩ tᶜ)ᶜ ∈ measurableCylinders α
-- Mathlib/FieldTheory/IntermediateField/Adjoin/Defs.lean
theorem adjoin_intCast (n : ℤ) : F⟮(n : E)⟯ = ⊥

Proof state:
F : Type u_1
inst✝² : Field F
E : Type u_2
inst✝¹ : Field E
inst✝ : Algebra F E
n : ℤ
⊢ F⟮↑n⟯ = ⊥

Tactic:
exact adjoin_simple_eq_bot_iff.mpr (intCast_mem ⊥ n)

Result:
no goals
-- Mathlib/Algebra/Group/Basic.lean
@[to_additive add_zsmul_self]
lemma mul_self_zpow (a : G) (n : ℤ) : a * a ^ n = a ^ (n + 1)

Proof state:
G : Type u_3
inst✝ : Group G
a : G
n : ℤ
⊢ a * a ^ n = a ^ (n + 1)

Tactic:
rw [Int.add_comm, zpow_add, zpow_one]

Result:
no goals
-- Mathlib/Data/Real/Hyperreal.lean
theorem st_neg (x : ℝ*) : st (-x) = -st x

Proof state:
x : ℝ*
⊢ (-x).st = -x.st

Tactic:
by_cases h : Infinite x

Result:
case pos
x : ℝ*
h : x.Infinite
⊢ (-x).st = -x.st

case neg
x : ℝ*
h : ¬x.Infinite
⊢ (-x).st = -x.st

Proof state:
case pos
x : ℝ*
h : x.Infinite
⊢ (-x).st = -x.st

Tactic:
rw [h.st_eq, (infinite_neg.2 h).st_eq, neg_zero]

Result:
no goals

Proof state:
case neg
x : ℝ*
h : ¬x.Infinite
⊢ (-x).st = -x.st

Tactic:
exact (isSt_st' (not_infinite_neg h)).unique (isSt_st' h).neg

Result:
no goals
-- Mathlib/LinearAlgebra/Matrix/Adjugate.lean
theorem mul_adjugate (A : Matrix n n α) : A * adjugate A = A.det • (1 : Matrix n n α)

Proof state:
case a
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
i j : n
⊢ (A * A.adjugate) i j = (A.det • 1) i j

Tactic:
rw [mul_apply, Pi.smul_apply, Pi.smul_apply, one_apply, smul_eq_mul, mul_boole]

Result:
case a
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
i j : n
⊢ ∑ j_1 : n, A i j_1 * A.adjugate j_1 j = if i = j then A.det else 0

Proof state:
case a
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
i j : n
⊢ ∑ j_1 : n, A i j_1 * A.adjugate j_1 j = if i = j then A.det else 0

Tactic:
simp [mul_adjugate_apply, sum_cramer_apply, cramer_transpose_row_self, Pi.single_apply, eq_comm]

Result:
no goals

Proof state:
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
⊢ A * A.adjugate = A.det • 1

Tactic:
ext i j

Result:
case a
n : Type v
α : Type w
inst✝² : DecidableEq n
inst✝¹ : Fintype n
inst✝ : CommRing α
A : Matrix n n α
i j : n
⊢ (A * A.adjugate) i j = (A.det • 1) i j
-- Mathlib/Analysis/Normed/Algebra/MatrixExponential.lean
theorem exp_conj' (U : Matrix m m 𝔸) (A : Matrix m m 𝔸) (hy : IsUnit U) :
    exp 𝕂 (U⁻¹ * A * U) = U⁻¹ * exp 𝕂 A * U :=
  let ⟨u, hu⟩ := hy
  hu ▸ by simpa only [Matrix.coe_units_inv] using exp_units_conj' 𝕂 u A

Proof state:
𝕂 : Type u_1
m : Type u_2
𝔸 : Type u_5
inst✝⁵ : RCLike 𝕂
inst✝⁴ : Fintype m
inst✝³ : DecidableEq m
inst✝² : NormedCommRing 𝔸
inst✝¹ : NormedAlgebra 𝕂 𝔸
inst✝ : CompleteSpace 𝔸
U A : Matrix m m 𝔸
hy : IsUnit U
u : (Matrix m m 𝔸)ˣ
hu : ↑u = U
⊢ exp 𝕂 ((↑u)⁻¹ * A * ↑u) = (↑u)⁻¹ * exp 𝕂 A * ↑u

Tactic:
simpa only [Matrix.coe_units_inv] using exp_units_conj' 𝕂 u A

Result:
no goals
-- Mathlib/Data/List/ToFinsupp.lean
theorem toFinsupp_nil [DecidablePred fun i => getD ([] : List M) i 0 ≠ 0] :
    toFinsupp ([] : List M) = 0

Proof state:
case h
M : Type u_1
inst✝¹ : Zero M
inst✝ : DecidablePred fun i => [].getD i 0 ≠ 0
a✝ : ℕ
⊢ [].toFinsupp a✝ = 0 a✝

Tactic:
simp

Result:
no goals

Proof state:
M : Type u_1
inst✝¹ : Zero M
inst✝ : DecidablePred fun i => [].getD i 0 ≠ 0
⊢ [].toFinsupp = 0

Tactic:
ext

Result:
case h
M : Type u_1
inst✝¹ : Zero M
inst✝ : DecidablePred fun i => [].getD i 0 ≠ 0
a✝ : ℕ
⊢ [].toFinsupp a✝ = 0 a✝
-- Mathlib/.lake/packages/lean4/src/lean/Std/Data/DHashMap/Internal/WF.lean
theorem wfImp_updateBucket_alter [BEq α] [Hashable α] [LawfulBEq α] {m : Raw₀ α β}
    (h : Raw.WFImp m.1) {a : α} {f : Option (β a) → Option (β a)} :
    Raw.WFImp (withComputedSize <| updateBucket m.1.buckets m.2 a (AssocList.alter a f)) where
  buckets_hash_self := isHashSelf_updateBucket_alter h
  size_eq

Proof state:
α : Type u
β : α → Type v
inst✝² : BEq α
inst✝¹ : Hashable α
inst✝ : LawfulBEq α
m : Raw₀ α β
h : Raw.WFImp m.val
a : α
f : Option (β a) → Option (β a)
⊢ (withComputedSize (updateBucket m.val.buckets ⋯ a (AssocList.alter a f))).size =
    (toListModel (withComputedSize (updateBucket m.val.buckets ⋯ a (AssocList.alter a f))).buckets).length

Tactic:
rw [size_withComputedSize, computeSize_eq, buckets_withComputedSize]

Result:
no goals
-- Mathlib/LinearAlgebra/Prod.lean
theorem range_coprod (f : M →ₗ[R] M₃) (g : M₂ →ₗ[R] M₃) : range (f.coprod g) = range f ⊔ range g :=
  Submodule.ext fun x => by simp [mem_sup]

Proof state:
R : Type u
M : Type v
M₂ : Type w
M₃ : Type y
inst✝⁶ : Semiring R
inst✝⁵ : AddCommMonoid M
inst✝⁴ : AddCommMonoid M₂
inst✝³ : AddCommMonoid M₃
inst✝² : Module R M
inst✝¹ : Module R M₂
inst✝ : Module R M₃
f : M →ₗ[R] M₃
g : M₂ →ₗ[R] M₃
x : M₃
⊢ x ∈ range (f.coprod g) ↔ x ∈ range f ⊔ range g

Tactic:
simp [mem_sup]

Result:
no goals
-- Mathlib/Topology/Bornology/Absorbs.lean
lemma _root_.Set.Finite.absorbs_biUnion {ι : Type*} {t : ι → Set α} {I : Set ι} (hI : I.Finite) :
    Absorbs M s (⋃ i ∈ I, t i) ↔ ∀ i ∈ I, Absorbs M s (t i)

Proof state:
M : Type u_1
α : Type u_2
inst✝¹ : Bornology M
inst✝ : SMul M α
s : Set α
ι : Type u_3
t : ι → Set α
I : Set ι
hI : I.Finite
⊢ Absorbs M s (⋃ i ∈ I, t i) ↔ ∀ i ∈ I, Absorbs M s (t i)

Tactic:
simp [Absorbs, hI]

Result:
no goals
-- Mathlib/SetTheory/Cardinal/Basic.lean
theorem exists_not_mem_of_length_lt {α : Type*} (l : List α) (h : ↑l.length < #α) :
    ∃ z : α, z ∉ l

Proof state:
α : Type u_1
l : List α
h : ∀ (z : α), z ∈ l
⊢ #α ≤ ↑l.length

Tactic:
calc
  #α = #(Set.univ : Set α) := mk_univ.symm
  _ ≤ #l.toFinset := mk_le_mk_of_subset fun x _ => List.mem_toFinset.mpr (h x)
  _ = l.toFinset.card := Cardinal.mk_coe_finset
  _ ≤ l.length := Nat.cast_le.mpr (List.toFinset_card_le l)

Result:
no goals

Proof state:
α : Type u_1
l : List α
h : ↑l.length < #α
⊢ ∃ z, z ∉ l

Tactic:
contrapose! h

Result:
α : Type u_1
l : List α
h : ∀ (z : α), z ∈ l
⊢ #α ≤ ↑l.length

Proof state:
α : Type u_1
l : List α
h : ↑l.length < #α
⊢ ∃ z, z ∉ l

Tactic:
classical
contrapose! h
calc
  #α = #(Set.univ : Set α) := mk_univ.symm
  _ ≤ #l.toFinset := mk_le_mk_of_subset fun x _ => List.mem_toFinset.mpr (h x)
  _ = l.toFinset.card := Cardinal.mk_coe_finset
  _ ≤ l.length := Nat.cast_le.mpr (List.toFinset_card_le l)

Result:
no goals
-- Mathlib/Order/Filter/Interval.lean
theorem tendstoIxxClass_inf {l₁ l₁' l₂ l₂' : Filter α} {Ixx} [h : TendstoIxxClass Ixx l₁ l₂]
    [h' : TendstoIxxClass Ixx l₁' l₂'] : TendstoIxxClass Ixx (l₁ ⊓ l₁') (l₂ ⊓ l₂') :=
  ⟨by simpa only [prod_inf_prod, smallSets_inf] using h.1.inf h'.1⟩

Proof state:
α : Type u_1
l₁ l₁' l₂ l₂' : Filter α
Ixx : α → α → Set α
h : TendstoIxxClass Ixx l₁ l₂
h' : TendstoIxxClass Ixx l₁' l₂'
⊢ Tendsto (fun p => Ixx p.1 p.2) ((l₁ ⊓ l₁') ×ˢ (l₁ ⊓ l₁')) (l₂ ⊓ l₂').smallSets

Tactic:
simpa only [prod_inf_prod, smallSets_inf] using h.1.inf h'.1

Result:
no goals
-- Mathlib/Combinatorics/SimpleGraph/Connectivity/WalkDecomp.lean
@[simp]
lemma takeUntil_first (p : G.Walk u v) :
    p.takeUntil u p.start_mem_support = .nil

Proof state:
V : Type u
G : SimpleGraph V
v u : V
inst✝ : DecidableEq V
p : G.Walk u v
⊢ p.takeUntil u ⋯ = nil

Tactic:
cases p <;> simp [Walk.takeUntil]

Result:
no goals
-- Mathlib/Data/Finset/Sum.lean
theorem disjSum_eq_empty : s.disjSum t = ∅ ↔ s = ∅ ∧ t = ∅

Proof state:
α : Type u_1
β : Type u_2
s : Finset α
t : Finset β
⊢ s.disjSum t = ∅ ↔ s = ∅ ∧ t = ∅

Tactic:
simp [Finset.ext_iff]

Result:
no goals
-- Mathlib/RingTheory/PiTensorProduct.lean
@[simp] lemma mul_tprod_tprod (x y : (i : ι) → A i) :
    mul (tprod R x) (tprod R y) = tprod R (x * y)

Proof state:
ι : Type u_1
R : Type u_3
A : ι → Type u_4
inst✝⁴ : CommSemiring R
inst✝³ : (i : ι) → NonUnitalNonAssocSemiring (A i)
inst✝² : (i : ι) → Module R (A i)
inst✝¹ : ∀ (i : ι), SMulCommClass R (A i) (A i)
inst✝ : ∀ (i : ι), IsScalarTower R (A i) (A i)
x y : (i : ι) → A i
⊢ (mul ((tprod R) x)) ((tprod R) y) = (tprod R) (x * y)

Tactic:
simp only [mul, piTensorHomMap₂_tprod_tprod_tprod, LinearMap.mul_apply', Pi.mul_def]

Result:
no goals
-- Mathlib/ModelTheory/PartialEquiv.lean
theorem le_partialEquivLimit (i : ι) : S i ≤ partialEquivLimit S :=
  ⟨le_iSup (f := fun i ↦ (S i).dom) _, by
    #adaptation_note /-- https://github.com/leanprover/lean4/pull/5020
    these two `simp` calls cannot be combined. -/
    simp only [partialEquivLimit_comp_inclusion]
    simp only [cod_partialEquivLimit, dom_partialEquivLimit, ← Embedding.comp_assoc,
      subtype_comp_inclusion]⟩

Proof state:
L : Language
M : Type w
N : Type w'
inst✝⁴ : L.Structure M
inst✝³ : L.Structure N
ι : Type u_1
inst✝² : Preorder ι
inst✝¹ : Nonempty ι
inst✝ : IsDirected ι fun x1 x2 => x1 ≤ x2
S : ι →o M ≃ₚ[L] N
i : ι
⊢ (partialEquivLimit S).cod.subtype.comp ((inclusion ⋯).comp (S i).toEquiv.toEmbedding) =
    (S i).cod.subtype.comp (S i).toEquiv.toEmbedding

Tactic:
simp only [cod_partialEquivLimit, dom_partialEquivLimit, ← Embedding.comp_assoc,
  subtype_comp_inclusion]

Result:
no goals

Proof state:
L : Language
M : Type w
N : Type w'
inst✝⁴ : L.Structure M
inst✝³ : L.Structure N
ι : Type u_1
inst✝² : Preorder ι
inst✝¹ : Nonempty ι
inst✝ : IsDirected ι fun x1 x2 => x1 ≤ x2
S : ι →o M ≃ₚ[L] N
i : ι
⊢ (partialEquivLimit S).cod.subtype.comp ((partialEquivLimit S).toEquiv.toEmbedding.comp (inclusion ⋯)) =
    (S i).cod.subtype.comp (S i).toEquiv.toEmbedding

Tactic:
simp only [partialEquivLimit_comp_inclusion]

Result:
L : Language
M : Type w
N : Type w'
inst✝⁴ : L.Structure M
inst✝³ : L.Structure N
ι : Type u_1
inst✝² : Preorder ι
inst✝¹ : Nonempty ι
inst✝ : IsDirected ι fun x1 x2 => x1 ≤ x2
S : ι →o M ≃ₚ[L] N
i : ι
⊢ (partialEquivLimit S).cod.subtype.comp ((inclusion ⋯).comp (S i).toEquiv.toEmbedding) =
    (S i).cod.subtype.comp (S i).toEquiv.toEmbedding
-- Mathlib/Data/Set/Prod.lean
theorem prod_sub_preimage_iff {W : Set γ} {f : α × β → γ} :
    s ×ˢ t ⊆ f ⁻¹' W ↔ ∀ a b, a ∈ s → b ∈ t → f (a, b) ∈ W

Proof state:
α : Type u_1
β : Type u_2
γ : Type u_3
s : Set α
t : Set β
W : Set γ
f : α × β → γ
⊢ s ×ˢ t ⊆ f ⁻¹' W ↔ ∀ (a : α) (b : β), a ∈ s → b ∈ t → f (a, b) ∈ W

Tactic:
simp [subset_def]

Result:
no goals
-- Mathlib/Data/Matrix/Basis.lean
@[simp]
lemma transpose_stdBasisMatrix (i : m) (j : n) (a : α) :
    (stdBasisMatrix i j a)ᵀ = stdBasisMatrix j i a

Proof state:
m : Type u_2
n : Type u_3
α : Type u_5
inst✝² : DecidableEq m
inst✝¹ : DecidableEq n
inst✝ : Zero α
i : m
j : n
a : α
⊢ (stdBasisMatrix i j a)ᵀ = stdBasisMatrix j i a

Tactic:
aesop (add unsafe unfold stdBasisMatrix)

Result:
no goals
-- Mathlib/LinearAlgebra/DirectSum/TensorProduct.lean
theorem directSumLeft_symm_lof_tmul (i : ι₁) (x : M₁ i) (y : M₂') :
    (directSumLeft R M₁ M₂').symm (DirectSum.lof R _ _ i (x ⊗ₜ[R] y)) =
      DirectSum.lof R _ _ i x ⊗ₜ[R] y

Proof state:
R : Type u
inst✝⁵ : CommSemiring R
ι₁ : Type v₁
inst✝⁴ : DecidableEq ι₁
M₁ : ι₁ → Type w₁
M₂' : Type w₂'
inst✝³ : (i₁ : ι₁) → AddCommMonoid (M₁ i₁)
inst✝² : AddCommMonoid M₂'
inst✝¹ : (i₁ : ι₁) → Module R (M₁ i₁)
inst✝ : Module R M₂'
i : ι₁
x : M₁ i
y : M₂'
⊢ (directSumLeft R M₁ M₂').symm ((lof R ι₁ (fun i => M₁ i ⊗[R] M₂') i) (x ⊗ₜ[R] y)) = (lof R ι₁ M₁ i) x ⊗ₜ[R] y

Tactic:
rw [LinearEquiv.symm_apply_eq, directSumLeft_tmul_lof]

Result:
no goals
-- Mathlib/ModelTheory/PartialEquiv.lean
theorem le_domRestrict (f g : M ≃ₚ[L] N) {A : L.Substructure M} (hf : f.dom ≤ A)
    (hg : A ≤ g.dom) (hfg : f ≤ g) : f ≤ g.domRestrict hg :=
  ⟨hf, by rw [← (subtype_toEquiv_inclusion hfg)]; rfl⟩

Proof state:
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f g : M ≃ₚ[L] N
A : L.Substructure M
hf : f.dom ≤ A
hg : A ≤ g.dom
hfg : f ≤ g
⊢ (g.domRestrict hg).cod.subtype.comp ((g.domRestrict hg).toEquiv.toEmbedding.comp (inclusion hf)) =
    f.cod.subtype.comp f.toEquiv.toEmbedding

Tactic:
rw [← (subtype_toEquiv_inclusion hfg)]

Result:
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f g : M ≃ₚ[L] N
A : L.Substructure M
hf : f.dom ≤ A
hg : A ≤ g.dom
hfg : f ≤ g
⊢ (g.domRestrict hg).cod.subtype.comp ((g.domRestrict hg).toEquiv.toEmbedding.comp (inclusion hf)) =
    g.cod.subtype.comp (g.toEquiv.toEmbedding.comp (inclusion ⋯))

Proof state:
L : Language
M : Type w
N : Type w'
inst✝¹ : L.Structure M
inst✝ : L.Structure N
f g : M ≃ₚ[L] N
A : L.Substructure M
hf : f.dom ≤ A
hg : A ≤ g.dom
hfg : f ≤ g
⊢ (g.domRestrict hg).cod.subtype.comp ((g.domRestrict hg).toEquiv.toEmbedding.comp (inclusion hf)) =
    g.cod.subtype.comp (g.toEquiv.toEmbedding.comp (inclusion ⋯))

Tactic:
rfl

Result:
no goals
-- Mathlib/.lake/packages/lean4/src/lean/Init/Data/Vector/Lemmas.lean
theorem any_beq' [BEq α] [PartialEquivBEq α] {xs : Vector α n} :
    (xs.any fun x => x == a) = xs.contains a

Proof state:
α : Type u_1
n : Nat
a : α
inst✝¹ : BEq α
inst✝ : PartialEquivBEq α
xs : Vector α n
⊢ (xs.any fun x => x == a) = xs.contains a

Tactic:
simp only [BEq.comm, any_beq]

Result:
no goals
-- Mathlib/MeasureTheory/Measure/Haar/Basic.lean
theorem haarMeasure_closure_self {K₀ : PositiveCompacts G} : haarMeasure K₀ (closure K₀) = 1

Proof state:
G : Type u_1
inst✝⁴ : Group G
inst✝³ : TopologicalSpace G
inst✝² : IsTopologicalGroup G
inst✝¹ : MeasurableSpace G
inst✝ : BorelSpace G
K₀ : PositiveCompacts G
⊢ (haarMeasure K₀) (closure ↑K₀) = 1

Tactic:
rw [K₀.isCompact.measure_closure, haarMeasure_self]

Result:
no goals
-- Mathlib/Data/ZMod/Basic.lean
lemma mul_val_inv (hmn : m.Coprime n) : (m * (m⁻¹ : ZMod n).val : ZMod n) = 1

Proof state:
case inl
m : ℕ
hmn : m.Coprime 0
⊢ ↑m * ↑(↑m)⁻¹.val = 1

Tactic:
simp [m.coprime_zero_right.1 hmn]

Result:
no goals

Proof state:
case inr
m n : ℕ
hmn : m.Coprime n
hn : n ≠ 0
⊢ ↑m * ↑(↑m)⁻¹.val = 1

Tactic:
haveI : NeZero n := ⟨hn⟩

Result:
case inr
m n : ℕ
hmn : m.Coprime n
hn : n ≠ 0
this : NeZero n
⊢ ↑m * ↑(↑m)⁻¹.val = 1

Proof state:
case inr
m n : ℕ
hmn : m.Coprime n
hn : n ≠ 0
this : NeZero n
⊢ ↑m * ↑(↑m)⁻¹.val = 1

Tactic:
rw [ZMod.natCast_zmod_val, ZMod.coe_mul_inv_eq_one _ hmn]

Result:
no goals

Proof state:
m n : ℕ
hmn : m.Coprime n
⊢ ↑m * ↑(↑m)⁻¹.val = 1

Tactic:
obtain rfl | hn := eq_or_ne n 0

Result:
case inl
m : ℕ
hmn : m.Coprime 0
⊢ ↑m * ↑(↑m)⁻¹.val = 1

case inr
m n : ℕ
hmn : m.Coprime n
hn : n ≠ 0
⊢ ↑m * ↑(↑m)⁻¹.val = 1
-- Mathlib/Algebra/Polynomial/Degree/Operations.lean
theorem eq_one_of_monic_natDegree_zero (hf : p.Monic) (hfd : p.natDegree = 0) : p = 1

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
hf : p.Monic
hfd : p.natDegree = 0
⊢ p = 1

Tactic:
rw [Monic.def, leadingCoeff, hfd] at hf

Result:
R : Type u
inst✝ : Semiring R
p : R[X]
hf : p.coeff 0 = 1
hfd : p.natDegree = 0
⊢ p = 1

Proof state:
R : Type u
inst✝ : Semiring R
p : R[X]
hf : p.coeff 0 = 1
hfd : p.natDegree = 0
⊢ p = 1

Tactic:
rw [eq_C_of_natDegree_eq_zero hfd, hf, map_one]

Result:
no goals
-- Mathlib/RingTheory/Localization/InvSubmonoid.lean
theorem surj'' (z : S) : ∃ (r : R) (m : M), z = r • (toInvSubmonoid M S m : S)

Proof state:
case intro.mk
R : Type u_1
inst✝³ : CommRing R
M : Submonoid R
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
z : S
r : R
m : ↥M
e : z * (algebraMap R S) ↑(r, m).2 = (algebraMap R S) r
⊢ z = r • ↑((toInvSubmonoid M S) m)

Tactic:
rw [Algebra.smul_def, ← e, mul_assoc]

Result:
case intro.mk
R : Type u_1
inst✝³ : CommRing R
M : Submonoid R
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
z : S
r : R
m : ↥M
e : z * (algebraMap R S) ↑(r, m).2 = (algebraMap R S) r
⊢ z = z * ((algebraMap R S) ↑(r, m).2 * ↑((toInvSubmonoid M S) m))

Proof state:
R : Type u_1
inst✝³ : CommRing R
M : Submonoid R
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
z : S
⊢ ∃ r m, z = r • ↑((toInvSubmonoid M S) m)

Tactic:
rcases IsLocalization.surj M z with ⟨⟨r, m⟩, e : z * _ = algebraMap R S r⟩

Result:
case intro.mk
R : Type u_1
inst✝³ : CommRing R
M : Submonoid R
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
z : S
r : R
m : ↥M
e : z * (algebraMap R S) ↑(r, m).2 = (algebraMap R S) r
⊢ ∃ r m, z = r • ↑((toInvSubmonoid M S) m)

Proof state:
case intro.mk
R : Type u_1
inst✝³ : CommRing R
M : Submonoid R
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
z : S
r : R
m : ↥M
e : z * (algebraMap R S) ↑(r, m).2 = (algebraMap R S) r
⊢ ∃ r m, z = r • ↑((toInvSubmonoid M S) m)

Tactic:
refine ⟨r, m, ?_⟩

Result:
case intro.mk
R : Type u_1
inst✝³ : CommRing R
M : Submonoid R
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
z : S
r : R
m : ↥M
e : z * (algebraMap R S) ↑(r, m).2 = (algebraMap R S) r
⊢ z = r • ↑((toInvSubmonoid M S) m)

Proof state:
case intro.mk
R : Type u_1
inst✝³ : CommRing R
M : Submonoid R
S : Type u_2
inst✝² : CommRing S
inst✝¹ : Algebra R S
inst✝ : IsLocalization M S
z : S
r : R
m : ↥M
e : z * (algebraMap R S) ↑(r, m).2 = (algebraMap R S) r
⊢ z = z * ((algebraMap R S) ↑(r, m).2 * ↑((toInvSubmonoid M S) m))

Tactic:
simp

Result:
no goals